let P be compact Subset of (TOP-REAL 2); :: thesis: ( |[(- 1),0]|,|[1,0]| realize-max-dist-in P implies ( W-min P = |[(- 1),0]| & W-max P = |[(- 1),0]| ) )
set M = W-most P;
assume A1: |[(- 1),0]|,|[1,0]| realize-max-dist-in P ; :: thesis: ( W-min P = |[(- 1),0]| & W-max P = |[(- 1),0]| )
then A2: W-most P = {|[(- 1),0]|} by Th77;
set f = proj2 | (W-most P);
A3: dom (proj2 | (W-most P)) = the carrier of ((TOP-REAL 2) | (W-most P)) by FUNCT_2:def 1;
A4: the carrier of ((TOP-REAL 2) | (W-most P)) = W-most P by PRE_TOPC:8;
A5: |[(- 1),0]| in {|[(- 1),0]|} by TARSKI:def 1;
A6: (proj2 | (W-most P)) .: the carrier of ((TOP-REAL 2) | (W-most P)) = Im ((proj2 | (W-most P)),|[(- 1),0]|) by A1, A4, Th77
.= {((proj2 | (W-most P)) . |[(- 1),0]|)} by A2, A3, A4, A5, FUNCT_1:59
.= {(proj2 . |[(- 1),0]|)} by A2, A5, FUNCT_1:49
.= {(|[(- 1),0]| `2)} by PSCOMP_1:def 6 ;
then A7: lower_bound (proj2 | (W-most P)) = |[(- 1),0]| `2 by SEQ_4:9;
A8: upper_bound (proj2 | (W-most P)) = |[(- 1),0]| `2 by A6, SEQ_4:9;
|[(- 1),0]| = |[(|[(- 1),0]| `1),(|[(- 1),0]| `2)]| by EUCLID:53;
hence ( W-min P = |[(- 1),0]| & W-max P = |[(- 1),0]| ) by A1, A7, A8, Lm16, Th75; :: thesis: verum