Theorem RC-4. RC basis for right division in Abelian groups.

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

The conclusion is a single axiom for Abelian groups in terms of x − y.

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

1 x = x 2 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}

4,3 x · e = x 6,5 x · (x · y) = y 7 (e · (((A · B) · C) · A)) · C = B → □

13,12  (x · (y · z)) · u = x · (y · (z · u))  [2,3,5,3,1,1,5]
24  e · (((A · B) · C) · (A · C)) = B → □  [7 :13]
25  x · x = e  [3 → 5]
29,28  (x · y) · x = e · y  [2,5,5,25,25,3,25 :4, flip]
34  x · y = e · (y · x)  [2,1,5,25,25,25,25 :29]
47,46  (x · y) · z = e · (y · (x · z))  [2,5,3,25,25,1,5]
55  C · (A · (B · (e · (A · C)))) = B → □  [24 :47,47,47,47,6,6]
130  x · (y · (z · (e · (y · x)))) = z  [2,25,25,5,34,3,5 :4, flip]
132  □  [130,55]