Theorem SD-2. Intersection in terms of set difference.

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

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

3,2 x − (y − x) = x 4 x − (x − y) = y − (y − x) 5 (x − y) − z = (x − z) − (y − z) 7,6 x · y = x − (x − y) 8 (A · B) · C = A · (B · C), A · B = B · A → □

9 (A − (A − B)) − ((A − (A − B)) − C) =

A − (A − (B − (B − C))) → □  [copy,8 :7,7,7,7,7,7 :4]
10  (x − y) − (z − y) = (x − z) − y  [flip 5]
11  (x − y) − y = x − y  [2 → 2]
14,13  (x − y) − (x − y) = y − y  [11 → 4 :3]
15  (x − y) − ((x − y) − x) = x − (y − (y − x))  [4 → 4, flip]
22,21  (x − (x − y)) − (y − (y − x)) = x − x  [4 → 13 :14]
23  x − x = y − y  [4 → 13 :22,14]
24  ((x − y) − z) − (y − z) = (x − y) − z  [11 → 5, flip]
28  (x − y) − ((z − x) − y) = x − y  [2 → 5, flip]
44  (x − (x − y)) − y = z − z  [5 → 23 :3]
48,47  x − (y − y) = x  [23 → 4 :3]
56,55  (x − x) − y = x − x  [47 → 2]

76 (A − (A − B)) − ((B − (B − A)) − C) =

A − (A − (B − (B − C))) → □  [4 → 9]
103 x − x = ((y − (y − z)) − u) − z [44 → 10 :56]
107,106 ((x − y) − z) − y = (x − y) − (z − y)  [11 → 10, flip]
112,111 (x − y) − (z − x) = x − (y − (z − x))  [2 → 10, flip]
126,125 (x − y) − x = x − x  [55 → 10, flip]
128  ((x − (x − y)) − z) − y = u − u  [flip 103]
132  x − (y − (y − x)) = x − y  [15 :126,48, flip]
148  (x − (y − z)) − y = x − y  [125 → 10 :48, flip]
153,152 x − (x − (x − y)) = x − y  [125 → 4 :48, flip]
178 (x − y) − (x − (y − z)) = z − z [148 → 125 :14,14]

227,226 ((x − (x − y)) − z) − ((y − x) − z) = (x − (x − y)) − z

[132 → 28]
294 (x − (x − y)) − z = (y − (y − x)) − z [4 → 24 :227]

313 x − (x − ((y − (y − x)) − z)) = (y − (y − x)) − z

[128 → 4 :48, flip]
403  x − (x − ((y − x) − z)) = z − z  [2 → 178]
521  x − (x − ((y − x) − z)) = x − x  [132 → 403 :14,14,14]
615,614 (x − y) − (z − y) = (x − y) − z  [521 → 132 :48,107, flip]

770  x − (y − (z − x)) = x − y  [28 :615,112]
774  (x − y) − z = (x − z) − y  [10 :615]
842,841 x − ((y − (z − x)) − u) = x − (y − u)  [774 → 770]
847,846 (x − (x − y)) − z = y − (y − (x − z))  [313 :842, flip]
861 x − (x − (y − z)) = y − (y − (x − z)) [294 :847,847]

862 B − (B − (A − (B − C))) = A − (A − (B − (B − C))) → □

[76 :847,847,153]

863  □  [862,861]