Theorem STN-4. Stein quasigroups under (gL).

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

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

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

9  (x · y) · (z · (z · u)) = z · (y · (x · u))  [5 → 5 :(gL) :6]
10  (x · (x · y)) · (y · z) = y · (x · z)  [5 → 5 :(gL)]
33  x · (x · y) = y · x  [4,10,9]
34  □  [33,1]