Theorem SD-1. Inconsistency of set difference with (gL).

\{ \begin{matrix}x − (y − x) = x \\ x − (x − y) = y − (y − x) \end{matrix} \} =(gL)⇒ \{x = y\}.

Proof (found by Otter 3.0.4 on gyro at 0.29 seconds).

1 A ≠ B 4,3 x − (y − x) = x 5 x − (x − y) = y − (y − x)

8,7  (x − y) − z = x − z  [3 → 3 :(gL)]
10,9  x − (y − (z − u)) = x − u  [3 → 7 :(gL), flip]
16,15  x − x = x  [5 → 5 :10,8,8,4]
18,17  x − y = y  [3 → 5 :16,8,16, flip]
19  x = y  [7 → 5 :18,18,18,18,18]
20  □  [19,1]