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:56 ;
hence LSeg (LMP P),|[0 ,(- 3)]| is vertical by SPPOL_1:37; :: thesis: verum