let P be compact Subset of (TOP-REAL 2); :: thesis: ( |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in P implies W-most P = {|[(- 1),0 ]|} )
assume A1: |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in P ; :: thesis: W-most P = {|[(- 1),0 ]|}
then A2: P c= closed_inside_of_rectangle (- 1),1,(- 3),3 by Th71;
set L = LSeg (SW-corner P),(NW-corner P);
A3: |[(- 1),0 ]| in P by A1, JORDAN24:def 1;
A4: (SW-corner P) `1 = |[(- 1),(S-bound P)]| `1 by A1, Th75
.= - 1 by EUCLID:56 ;
A5: (NW-corner P) `1 = |[(- 1),(N-bound P)]| `1 by A1, Th75
.= - 1 by EUCLID:56 ;
thus W-most P c= {|[(- 1),0 ]|} :: according to XBOOLE_0:def 10 :: thesis: {|[(- 1),0 ]|} c= W-most P

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in W-most P or x in {|[(- 1),0 ]|} )
assume A6: x in W-most P ; :: thesis: x in {|[(- 1),0 ]|}
then A7: x in P by XBOOLE_0:def 4;
reconsider x = x as Point of (TOP-REAL 2) by A6;
A8: x in LSeg (SW-corner P),(NW-corner P) by A6, XBOOLE_0:def 4;
SW-corner P in LSeg (SW-corner P),(NW-corner P) by RLTOPSP1:69;
then A9: x `1 = - 1 by A4, A8, SPPOL_1:def 3;
x in closed_inside_of_rectangle (- 1),1,(- 3),3 by A2, A7;
then ex p being Point of (TOP-REAL 2) st
( x = p & - 1 <= p `1 & p `1 <= 1 & - 3 <= p `2 & p `2 <= 3 ) ;
then x in rectangle (- 1),1,(- 3),3 by A9, Lm59;
then x in P /\ (rectangle (- 1),1,(- 3),3) by A7, XBOOLE_0:def 4;
then x in {|[(- 1),0 ]|,|[1,0 ]|} by A1, Th74;
then ( x = |[(- 1),0 ]| or x = |[1,0 ]| ) by TARSKI:def 2;
hence x in {|[(- 1),0 ]|} by A9, EUCLID:56, TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {|[(- 1),0 ]|} or x in W-most P )
assume x in {|[(- 1),0 ]|} ; :: thesis: x in W-most P
then A10: x = |[(- 1),0 ]| by TARSKI:def 1;
A11: (SW-corner P) `2 = S-bound P by EUCLID:56;
(NW-corner P) `2 = N-bound P by EUCLID:56;
then ( (SW-corner P) `2 <= |[(- 1),0 ]| `2 & |[(- 1),0 ]| `2 <= (NW-corner P) `2 ) by A3, A11, PSCOMP_1:71;
then |[(- 1),0 ]| in LSeg (SW-corner P),(NW-corner P) by A4, A5, Lm18, GOBOARD7:8;
hence x in W-most P by A3, A10, XBOOLE_0:def 4; :: thesis: verum