Theorem MED-5. Median law for four group operations.

\{ \begin{matrix}e(ex) = x \\ ee = e \\ e(xe) = (ex)e \end{matrix} \} =(gL)⇒ \{(xy)(zu) = (xz)(yu)\}.

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

3,2 e · (e · x) = x 4 e · e = e 6 e · (x · e) = (e · x) · e

7 (e · x) · e = e · (x · e) [flip 6]

9 (A · C) · (B · D) ≠ (A · B) · (C · D)

10  (e · x) · (e · y) = e · (x · y)  [4 → 7 :(gL)]
12  (x · y) · e = (x · e) · (y · e)  [4 → 7 :(gL)]
23  x · (y · e) = e · (y · (x · e))  [7 → 10 :(gL) :3]
25  (x · e) · (y · e) = (x · y) · e  [12 → 2 :3]
28  x · ((y · e) · z) = e · ((y · x) · z)  [12 → 23 :(gL)]
29  e · (x · (y · e)) = y · (x · e)  [23 → 2 :3]
49  x · ((y · z) · e) = e · ((y · x) · (z · e))  [25 → 28]
66  (x · y) · (z · e) = (x · z) · (y · e)  [49 → 29 :3]
67  (x · y) · (z · u) = (x · z) · (y · u)  [2 → 66 :(gL) :3]
68  □  [67,9]