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

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

Proof (found by Otter 3.0.4 on gyro at 0.48 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)

6  (x · y) · (z · u) = x · (y · (z · u))  [flip 5]
13  (x · y) · (z · u) = x · ((y · z) · u)  [6 → 6 :(gL)]
15  (x · y) · (z · u) = x · (z · (y · u))  [(gL) 6]
42  (x · y) · z = y · (x · z)  [3,13,15, flip]
91  x · y = y · x  [4,15,42]
92  □  [91,1]