Theorem MED-4. Median law for chord-tangent construction (3).

{x(ex) = e} =(gL)⇒ {(xy)(zu) = (xz)(yu)}.

Proof (found by Otter 3.0.4 on gyro at 1.30 seconds). 2 x · (e · x) = e 4 (A · C) · (B · D) ≠ (A · B) · (C · D)

7  x · (y · x) = z · (y · z)  [2 → 2 :(gL)]
8  (x · y) · (z · (x · z)) = u · (y · u)  [7 → 7]
67  (x · y) · (z · u) = (x · z) · (y · u)  [(gL) 8]
68  □  [67,4]