Theorem CS-GL-7. Nearly (5) associative cancellative (gL)-groupoids are commutative.

\{ \begin{matrix}cancellation \\ (x(yz))u = (xy)(zu) \end{matrix} \} =(gL)⇒ \{xy = yx\}.

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

1 B · A = A · B → □ 3 x · y = z, x · u = z → y = u 4 x · y = z, u · y = z → x = u 5 (x · (y · z)) · u = (x · y) · (z · u)

8  ((x · (y · z)) · u) · v = ((x · y) · z) · (u · v)  [5 → 5]
24  ((x · (y · z)) · u) · v = ((x · y) · u) · (z · v)  [(gL) 8]
29  (x · (y · z)) · u = (x · z) · (y · u)  [5 → 24 :(gL)]
32  (x · y) · (z · u) = (x · z) · (y · u)  [8 → 24 :(gL)]
67  x · (y · z) = x · (z · y)  [4,5,29]
183  x · y = y · x  [3,32,67]
184  □  [183,1]