Theorem CS-GL-2. Diassociative cancellative (gL)-groupoids are commutative.

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

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

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

12  (x · x) · (y · z) = x · ((x · y) · z)  [6 → 5 :(gL)]
13  x · ((y · z) · u) = x · (y · (z · u))  [5 → 12 :(gL), flip]
14  (x · x) · (y · z) = x · (y · (x · z))  [5 → 12 :(gL)]
19  (x · y) · z = x · (y · z)  [3,2,13, flip]
22  (x · y) · z = y · (x · z)  [3,12,14, flip]
38  x · y = y · x  [4,19,22]
39  □  [38,1]