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;
A4: (SW-corner P) `1 =
|[(- 1),(S-bound P)]| `1
by A1, Th75
.=
- 1
by EUCLID:52
;
A5: (NW-corner P) `1 =
|[(- 1),(N-bound P)]| `1
by A1, Th75
.=
- 1
by EUCLID:52
;
thus
W-most P c= {|[(- 1),0]|}
XBOOLE_0:def 10 {|[(- 1),0]|} c= W-most Pproof
let x be
object ;
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:68;
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:52, TARSKI:def 1;
verum
end;
let x be object ; 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:52;
A12:
(NW-corner P) `2 = N-bound P
by EUCLID:52;
A13:
(SW-corner P) `2 <= |[(- 1),0]| `2
by A3, A11, PSCOMP_1:24;
|[(- 1),0]| `2 <= (NW-corner P) `2
by A3, A12, PSCOMP_1:24;
then
|[(- 1),0]| in LSeg ((SW-corner P),(NW-corner P))
by A4, A5, A13, Lm16, GOBOARD7:7;
hence
x in W-most P
by A3, A10, XBOOLE_0:def 4; verum