let P be Subset of (TOP-REAL 2); :: thesis: LSeg (LMP P),|[(((W-bound P) + (E-bound P)) / 2),(S-bound P)]| is vertical
set w = ((W-bound P) + (E-bound P)) / 2;
A1: |[(((W-bound P) + (E-bound P)) / 2),(S-bound P)]| `1 = ((W-bound P) + (E-bound P)) / 2 by EUCLID:56;
(LMP P) `1 = ((W-bound P) + (E-bound P)) / 2 by EUCLID:56;
hence LSeg (LMP P),|[(((W-bound P) + (E-bound P)) / 2),(S-bound P)]| is vertical by A1, SPPOL_1:37; :: thesis: verum