Theorem TC-12. TC Steiner quasigroups with xe = ex are Abelian groups.

\{ \begin{matrix}TC \\ f(x, y) = e · (y · x) \\ x · (y · x) = y \\ x · e = e · x \end{matrix} \} ⇒ \{ \begin{matrix}f(x, y) = f(y, x) \\ f(f(x, y), z) = f(x, f(y, z)) \\ f(e, x) = x \\ ∀y∃x, f(x, y) = e \end{matrix} \} .

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

1 x = x 2 x · y = z, u · v = z, x · w = v_{6}, v_{7} · v = v_{6} → u · w = v_{7} · y 3 f(B, A) = f(A, B), f(f(A, B), C) = f(A, f(B, C)),

f(e, A) = A, f(x, A) = e → □

5,4 x · (y · x) = y 6 x · e = e · x 8,7 f(x, y) = e · (y · x)

10 e · (B · A) = e · (A · B), e · ((e · (C · B)) · A) = e · (C · (e · (B · A))),

e · (A · x) = e → □  [3 :8,8,8,8,8,8,8,5,8 :1, flip,flip]
17,16 (x · y) · x = y  [4 → 4]
19  x · y = y · x  [2,4,6,1,6 :17]
115  x · (x · y) = y  [16 → 19, flip]
117  (x · y) · y = x  [4 → 19, flip]
119  x · (y · z) = x · (z · y)  [2,115,115,4,115]
243,242 (x · (y · z)) · u = y · (x · (z · u))  [2,117,115,4,117, flip]
348  e · (A · x) = e → □  [10 :243 :119,1]
349  e · x = e → □  [115 → 348]
350  □  [349,115]