let P be compact Subset of (TOP-REAL 2); ( |[(- 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
; 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;
A4: (SE-corner P) `1 =
|[1,(S-bound P)]| `1
by A1, Th76
.=
1
by EUCLID:52
;
A5: (NE-corner P) `1 =
|[1,(N-bound P)]| `1
by A1, Th76
.=
1
by EUCLID:52
;
thus
E-most P c= {|[1,0]|}
XBOOLE_0:def 10 {|[1,0]|} c= E-most Pproof
let x be
object ;
TARSKI:def 3 ( not x in E-most P or x in {|[1,0]|} )
assume A6:
x in E-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 (
(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: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 E-most P )
assume
x in {|[1,0]|}
; x in E-most P
then A10:
x = |[1,0]|
by TARSKI:def 1;
A11:
(SE-corner P) `2 = S-bound P
by EUCLID:52;
A12:
(NE-corner P) `2 = N-bound P
by EUCLID:52;
A13:
(SE-corner P) `2 <= |[1,0]| `2
by A3, A11, PSCOMP_1:24;
|[1,0]| `2 <= (NE-corner P) `2
by A3, A12, PSCOMP_1:24;
then
|[1,0]| in LSeg ((SE-corner P),(NE-corner P))
by A4, A5, A13, Lm17, GOBOARD7:7;
hence
x in E-most P
by A3, A10, XBOOLE_0:def 4; verum