Theorem TC-14. Set difference is inconsistent with TC.

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

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

1 A = B → □ 2 x = x 3 x − y = z, u − v = z, x − w = v_{6}, v_{7} − v = v_{6} → u − w = v_{7} − y 5,4 x − (y − x) = x 6 x − (x − y) = y − (y − x)

9,8  (x − y) − y = x − y  [4 → 4]
11,10 x − (y − (x − z)) = x − z  [3,8,2,4,8 :9]
14 (x − y) − ((x − y) − z) = z − y [3,8,4,2,6]
41,40 (x − y) − (z − ((u − y) − v)) = (u − y) − v  [3,10,10,14,14 :11, flip]
44,43 (x − y) − ((z − y) − x) = x − y  [3,10,2,8,14 :9,41, flip]
49,48 x − y = x  [3,14,10,14,4 :5,44, flip]
50  x = y  [3,14,8,14,8 :49,49,49,49,49,49,49,49]
51  □  [50,1]