let P be Subset of (TOP-REAL 2); :: thesis: ( |[(- 1),0]|,|[1,0]| realize-max-dist-in P implies LSeg ((LMP P),|[0,(- 3)]|) is vertical )
assume |[(- 1),0]|,|[1,0]| realize-max-dist-in P ; :: thesis: LSeg ((LMP P),|[0,(- 3)]|) is vertical
then |[0,(- 3)]| `1 = ((W-bound P) + (E-bound P)) / 2 by Lm88
.= (LMP P) `1 by EUCLID:52 ;
hence LSeg ((LMP P),|[0,(- 3)]|) is vertical by SPPOL_1:16; :: thesis: verum