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