Theorem MFL-3. Moufang-3 ⇒ Moufang-1 in loops.

\{ \begin{matrix}loop \\ ((x · y) · x) · z = x · (y · (x · z)) \end{matrix} \} ⇒ \{(x · (y · z)) · x = (x · y) · (z · x)\}.

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

3,2 1 · x = x 5,4 x · 1 = x 7,6 x · (x\y) = y 12 (x · y)/y = x 14 x · R(x) = 1 16 L(x) · x = 1 18 ((x · y) · x) · z = x · (y · (x · z)) 20 (A · (B · C)) · A ≠ (A · B) · (C · A)

40,39  1/x = L(x)  [16 → 12]
41  L(R(x)) = x  [14 → 12 :40]
47  L(x) · (x · (L(x) · y)) = L(x) · y  [16 → 18 :3, flip]
60,59  (x · y) · x = x · (y · x)  [4 → 18 :5]
65  A · ((B · C) · A) ≠ (A · B) · (C · A)  [20 :60]
66  (x · (y · x)) · z = x · (y · (x · z))  [18 :60]
92  L(x) · (x · y) = y  [6 → 47 :7]
95,94  x · (R(x) · y) = y  [41 → 92]
102  L(L(x)) = x  [16 → 92 :5]
105,104 L(x) = R(x)  [14 → 92 :5]
111,110 R(x) · x = 1  [4 → 92 :105]
115,114 R(R(x)) = x  [102 :105,105]
120  R(x) · (x · y) = y  [92 :105]
136  x · ((R(x) · y) · x) = y · x  [94 → 59, flip]
156  x/(y · x) = R(y)  [120 → 12]
190  (x · (y · (x · z)))/z = x · (y · x)  [66 → 12]
204  (x · R(y)) · y = x  [66 → 136 :111,5,95, flip]
222  (x · y) · R(y) = x  [114 → 204]
233,232 x/y = R(y · R(x))  [204 → 156]
238,237 R(x · R(y)) = y · R(x)  [204 → 12 :233]
243  (x · (y · (x · z))) · R(z) = x · (y · x)  [190 :233,238]
256  x · R(y · x) = R(y)  [120 → 222]
267,266 R(x · y) = R(y) · R(x)  [222 → 256, flip]
440  (x · (y · z)) · (R(z) · x) = x · (y · x)  [94 → 243 :267,115]
552  (x · y) · (z · x) = x · ((y · z) · x)  [222 → 440 :115]
559  x · ((y · z) · x) = (x · y) · (z · x)  [flip 552]
560  □  [559,65]