Theorem RC-6. Set difference is inconsistent with RC.

\{ \begin{matrix}RC \\ 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.79 seconds).

1 A = B → □ 2 x = x 3 x − y = z, u − v = z, w − y = v_{6}, v_{7} − v = v_{6}, x − v_{8} = v_{9},

u − v_{10} = v_{9} → w − v_{8} = v_{7} − v_{10}

5,4 x − (y − x) = x 6 x − (x − y) = y − (y − x)

9,8  (x − y) − y = x − y  [4 → 4]
15,14  x − (y − (z − u)) = x − u  [3,8,8,2,8,4,8 :9]
17,16  (x − y) − z = x − z  [3,2,2,8,2,8,8]
23,22  x − y = x  [3,16,6,6,6,2,6 :17,5,15, flip]
24  x = y  [3,16,6,6,2,16,6 :23,23,23,23]
25  □  [24,1]