Theorem ABGT-2. Identity with (gL) is a commutative monoid.

\{ \begin{matrix}ex = x \\ xe = x \end{matrix} \} =(gL)⇒ \{ \begin{matrix}xy = yx \\ (xy)z = x(yz) \end{matrix} \} .

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

2 B · A = A · B, (A · B) · C = A · (B · C) → □ 3 e · x = x 4 x · e = x

5  (e · e) · x = x  [3 → 3]
7  (x · e) · e = x  [4 → 4]
8  (e · x) · e = x  [3 → 4]
83  (x · y) · e = (e · y) · x  [5 → 7 :(gL)]
153  (e · x) · y = x · y  [4 → 8 :(gL)]
201  (x · (y · z)) · e = (x · y) · z  [8 → 153 :(gL), flip]
384  x · y = (e · y) · x  [4 → 83]
884  (x · y) · z = x · (y · z)  [4 → 201, flip]
1078  x · y = y · x  [3 → 384]
1112  □  [2,1078,884]