let P be compact Subset of (TOP-REAL 2); :: thesis: ( |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in P implies E-most P = {|[1,0 ]|} )
assume A1:
|[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in P
; :: thesis: E-most P = {|[1,0 ]|}
then A2:
P c= closed_inside_of_rectangle (- 1),1,(- 3),3
by Th71;
set L = LSeg (SE-corner P),(NE-corner P);
A3:
|[1,0 ]| in P
by A1, JORDAN24:def 1;
A4: (SE-corner P) `1 =
|[1,(S-bound P)]| `1
by A1, Th76
.=
1
by EUCLID:56
;
A5: (NE-corner P) `1 =
|[1,(N-bound P)]| `1
by A1, Th76
.=
1
by EUCLID:56
;
thus
E-most P c= {|[1,0 ]|}
:: according to XBOOLE_0:def 10 :: thesis: {|[1,0 ]|} c= E-most Pproof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in E-most P or x in {|[1,0 ]|} )
assume A6:
x in E-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 (SE-corner P),
(NE-corner P)
by A6, XBOOLE_0:def 4;
SE-corner P in LSeg (SE-corner P),
(NE-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 E-most P )
assume
x in {|[1,0 ]|}
; :: thesis: x in E-most P
then A10:
x = |[1,0 ]|
by TARSKI:def 1;
A11:
(SE-corner P) `2 = S-bound P
by EUCLID:56;
(NE-corner P) `2 = N-bound P
by EUCLID:56;
then
( (SE-corner P) `2 <= |[1,0 ]| `2 & |[1,0 ]| `2 <= (NE-corner P) `2 )
by A3, A11, PSCOMP_1:71;
then
|[1,0 ]| in LSeg (SE-corner P),(NE-corner P)
by A4, A5, Lm19, GOBOARD7:8;
hence
x in E-most P
by A3, A10, XBOOLE_0:def 4; :: thesis: verum