let P be compact Subset of (TOP-REAL 2); ( |[(- 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
; 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 ]|}
XBOOLE_0:def 10 {|[(- 1),0 ]|} c= W-most Pproof
let x be
set ;
TARSKI:def 3 ( not x in W-most P or x in {|[(- 1),0 ]|} )
assume A6:
x in W-most P
;
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, Lm61;
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;
verum
end;
let x be set ; TARSKI:def 3 ( not x in {|[(- 1),0 ]|} or x in W-most P )
assume
x in {|[(- 1),0 ]|}
; 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;
A12:
(NW-corner P) `2 = N-bound P
by EUCLID:56;
A13:
(SW-corner P) `2 <= |[(- 1),0 ]| `2
by A3, A11, PSCOMP_1:71;
|[(- 1),0 ]| `2 <= (NW-corner P) `2
by A3, A12, PSCOMP_1:71;
then
|[(- 1),0 ]| in LSeg (SW-corner P),(NW-corner P)
by A4, A5, A13, Lm16, GOBOARD7:8;
hence
x in W-most P
by A3, A10, XBOOLE_0:def 4; verum