let P be Subset of (TOP-REAL 2); :: thesis: ( |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in P implies |[0 ,(- 3)]| `1 = ((W-bound P) + (E-bound P)) / 2 )
assume |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in P ; :: thesis: |[0 ,(- 3)]| `1 = ((W-bound P) + (E-bound P)) / 2
then ( W-bound P = - 1 & E-bound P = 1 ) by Th75, Th76;
hence |[0 ,(- 3)]| `1 = ((W-bound P) + (E-bound P)) / 2 by EUCLID:56; :: thesis: verum