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

{x(yx) = y} =(gL)⇒ {(xy)(zu) = (xz)(yu)}.

Proof (found by Otter 3.0.4 on gyro at 24.07 seconds). 2 x · (y · x) = y 3 (A · C) · (B · D) ≠ (A · B) · (C · D)

4  (x · (y · x)) · (z · y) = z  [2 → 2]
9  (x · y) · x = y  [2 → 2]
38  (x · (y · x)) · (z · y) = (u · z) · u  [9 → 4]
369  (x · (y · z)) · (u · y) = (x · u) · z  [(gL) 38]
371  (x · y) · (z · u) = (x · z) · (y · u)  [2 → 369]
372  □  [371,3]