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