Theorem MED-6. Median (gL)-algebras.

\{ \begin{matrix}(xy)(zu) = (xz)(yu) \\ ee = e \end{matrix} \} =(gL)⇒ \{(x(yz))((uv)w) = (x(uz))((yv)w)\}.

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

2 (x · y) · (z · u) = (x · z) · (y · u) 4,3 e · e = e 5 (A · (D · C)) · ((B · E) · F) ≠ (A · (B · C)) · ((D · E) · F)

6  (A · (B · C)) · ((D · E) · F) ≠ (A · (D · C)) · ((B · E) · F)  [flip 5]
7  ((x · y) · (z · u)) · (v · w) = ((x · z) · v) · ((y · u) · w)  [2 → 2]
11  (x · e) · (y · e) = (x · y) · e  [3 → 2]
17  (e · x) · e = e · (x · e)  [3 → 11 :4,4, flip]
54,53  ((e · x) · y) · (e · z) = (e · (x · e)) · (y · z)  [17 → 2]

128 (x · (y · z)) · ((u · v) · w) = (x · (u · z)) · ((y · v) · w)

[17 → 7 :54 :(gL) :(gL)]

129  □  [128,6]