Theorem ABGT-4. A (gL)-basis for right division in Abelian groups (1).

\{ \begin{matrix}x/(x/y) = y \\ x/x = e \end{matrix} \} =(gL)⇒ \{(x/((x/y)/z))/y = z\}.

Here, x/y is right division, and the conclusion is a single axiom for Abelian groups in terms of right division.

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

2 x/x = e 3 x/(x/y) = y 8 (A/((A/B)/C))/B ≠ C

22  x/e = x  [2 → 3]
26  (x/e)/e = x  [22 → 22]
27  (x/(x/y))/e = y  [3 → 22]
167  (x/e)/y = x/y  [22 → 26 :(gL)]
239  ((x/y)/z)/e = (x/z)/y  [26 → 167 :(gL), flip]
3177  (x/((x/y)/z))/y = z  [239 → 27]
3178  □  [3177,8]