let P be Subset of (TOP-REAL 2); :: thesis: ( |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in P implies W-bound P = - 1 )
assume A1: |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in P ; :: thesis: W-bound P = - 1
then A2: P c= closed_inside_of_rectangle (- 1),1,(- 3),3 by Th71;
A3: P = the carrier of ((TOP-REAL 2) | P) by PRE_TOPC:29;
A4: |[(- 1),0 ]| in P by A1, JORDAN24:def 1;
reconsider P = P as non empty Subset of (TOP-REAL 2) by A1, JORDAN24:def 1;
reconsider Z = (proj1 | P) .: the carrier of ((TOP-REAL 2) | P) as Subset of REAL ;
A5: for p being real number st p in Z holds
p >= - 1

proof

let p be real number ; :: thesis: ( p in Z implies p >= - 1 )
assume p in Z ; :: thesis: p >= - 1
then consider p0 being set such that
A6: p0 in the carrier of ((TOP-REAL 2) | P) and
p0 in the carrier of ((TOP-REAL 2) | P) and
A7: p = (proj1 | P) . p0 by FUNCT_2:115;
p0 in closed_inside_of_rectangle (- 1),1,(- 3),3 by A2, A3, A6;
then ex p1 being Point of (TOP-REAL 2) st
( p0 = p1 & - 1 <= p1 `1 & p1 `1 <= 1 & - 3 <= p1 `2 & p1 `2 <= 3 ) ;
hence p >= - 1 by A3, A6, A7, PSCOMP_1:69; :: thesis: verum

end;

for q being real number st ( for p being real number st p in Z holds
p >= q ) holds
- 1 >= q

proof

let q be real number ; :: thesis: ( ( for p being real number st p in Z holds
p >= q ) implies - 1 >= q )
assume A8: for p being real number st p in Z holds
p >= q ; :: thesis: - 1 >= q
(proj1 | P) . |[(- 1),0 ]| = |[(- 1),0 ]| `1 by A4, PSCOMP_1:69;
hence - 1 >= q by A3, A4, A8, Lm18, FUNCT_2:43; :: thesis: verum

end;

hence W-bound P = - 1 by A5, SEQ_4:61; :: thesis: verum