Theorem ABGT-1. (gL)-groups are Abelian.

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

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

2 e · x = x 3 x · e = x 4 x′ · x = e 5 x · x′ = e 6 (x · y) · z = x · (y · z) 7 B · A ≠ A · B

21  e · x = x · e  [3 → 2]
26  (x · e)′ · x = e  [3 → 4]
30  (e · x)′ · x = e  [2 → 4]
41,40  e′ = e  [3 → 4]
45  x′ · x = e · e  [3 → 4]
48,47  (e · e)′ = e  [3 → 40]
56,55  x · (x · e)′ = e  [3 → 5]
85,84  x · (e · y) = x · y  [3 → 6, flip]
102,101 (x · y) · z = e · (x · (y · z))  [2 → 6]
103  (x · y)′ · x = (z · y)′ · z  [26 → 26 :(gL)]
104  (x · y)′ · y = (x · z)′ · z  [30 → 30 :(gL)]
106,105 (x · y)′ · x = e · y′  [45 → 103 :48, flip]
112,111 (x · e)′ · e = e · x′  [21 → 103 :106]
116,115 (e · x)′ = e · x′  [3 → 103 :106]
119,118 (x · y)′ · y = e · x′  [55 → 104 :56,112, flip]
120 e · x′′ = e · x [45 → 104 :116,41,102,85,85,119, flip]
137,136 x′′ = e · x  [2 → 120]
140  e · (x · y) = e · (y · x)  [105 → 118 :116,137,85,102,85,137,85]
144  x · y = e · (y · x)  [2 → 140]
155  x · y = y · x  [2 → 144]
156  □  [155,7]