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:52; :: thesis: verum