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 A1: |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in P ; :: thesis: |[0 ,3]| `1 = ((W-bound P) + (E-bound P)) / 2
then A2: W-bound P = - 1 by Th75;
E-bound P = 1 by A1, Th76;
hence |[0 ,3]| `1 = ((W-bound P) + (E-bound P)) / 2 by A2, EUCLID:56; :: thesis: verum