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;
( |[(((W-bound P) + (E-bound P)) / 2),(S-bound P)]| `1 = ((W-bound P) + (E-bound P)) / 2 & (LMP P) `1 = ((W-bound P) + (E-bound P)) / 2 ) by EUCLID:52;
hence LSeg ((LMP P),|[(((W-bound P) + (E-bound P)) / 2),(S-bound P)]|) is vertical by SPPOL_1:16; :: thesis: verum