let P be Subset of (TOP-REAL 2); ( |[(- 1),0]|,|[1,0]| realize-max-dist-in P implies E-bound P = 1 )
assume A1:
|[(- 1),0]|,|[1,0]| realize-max-dist-in P
; E-bound P = 1
then A2:
P c= closed_inside_of_rectangle ((- 1),1,(- 3),3)
by Th71;
A3:
|[1,0]| in P
by A1;
reconsider P = P as non empty Subset of (TOP-REAL 2) by A1;
reconsider Z = (proj1 | P) .: the carrier of ((TOP-REAL 2) | P) as Subset of REAL ;
A4:
P = the carrier of ((TOP-REAL 2) | P)
by PRE_TOPC:8;
A5:
for p being Real st p in Z holds
p <= 1
for q being Real st ( for p being Real st p in Z holds
p <= q ) holds
1 <= q
hence
E-bound P = 1
by A5, SEQ_4:46; verum