let P be Subset of (TOP-REAL 2); :: thesis: ( |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in P implies P /\ (rectangle (- 1),1,(- 3),3) = {|[(- 1),0 ]|,|[1,0 ]|} )
assume A1:
|[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in P
; :: thesis: P /\ (rectangle (- 1),1,(- 3),3) = {|[(- 1),0 ]|,|[1,0 ]|}
then A2:
( |[(- 1),0 ]| in P & |[1,0 ]| in P )
by JORDAN24:def 1;
thus
P /\ (rectangle (- 1),1,(- 3),3) c= {|[(- 1),0 ]|,|[1,0 ]|}
:: according to XBOOLE_0:def 10 :: thesis: {|[(- 1),0 ]|,|[1,0 ]|} c= P /\ (rectangle (- 1),1,(- 3),3)proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in P /\ (rectangle (- 1),1,(- 3),3) or x in {|[(- 1),0 ]|,|[1,0 ]|} )
assume A3:
x in P /\ (rectangle (- 1),1,(- 3),3)
;
:: thesis: x in {|[(- 1),0 ]|,|[1,0 ]|}
then A4:
x in P
by XBOOLE_0:def 4;
x in rectangle (- 1),1,
(- 3),3
by A3, XBOOLE_0:def 4;
then A5:
(
x in (LSeg |[(- 1),(- 3)]|,|[(- 1),3]|) \/ (LSeg |[(- 1),3]|,|[1,3]|) or
x in (LSeg |[1,3]|,|[1,(- 3)]|) \/ (LSeg |[1,(- 3)]|,|[(- 1),(- 3)]|) )
by Lm38, XBOOLE_0:def 3;
reconsider x =
x as
Point of
(TOP-REAL 2) by A3;
per cases
( x in LSeg |[(- 1),(- 3)]|,|[(- 1),3]| or x in LSeg |[(- 1),3]|,|[1,3]| or x in LSeg |[1,3]|,|[1,(- 3)]| or x in LSeg |[1,(- 3)]|,|[(- 1),(- 3)]| )
by A5, XBOOLE_0:def 3;
suppose A6:
x in LSeg |[(- 1),(- 3)]|,
|[(- 1),3]|
;
:: thesis: x in {|[(- 1),0 ]|,|[1,0 ]|}
|[(- 1),(- 3)]| in LSeg |[(- 1),(- 3)]|,
|[(- 1),3]|
by RLTOPSP1:69;
then A7:
x `1 = - 1
by A6, Lm28, Lm43, SPPOL_1:def 3;
per cases
( x `2 = 0 or x `2 <> 0 )
;
suppose
x `2 <> 0
;
:: thesis: x in {|[(- 1),0 ]|,|[1,0 ]|}then A8:
(x `2 ) ^2 > 0
by SQUARE_1:74;
A9:
dist |[1,0 ]|,
x =
sqrt (((1 - (- 1)) ^2 ) + ((0 - (x `2 )) ^2 ))
by A7, Lm19, Lm21, TOPREAL6:101
.=
sqrt (4 + ((x `2 ) ^2 ))
;
0 + 4
< ((x `2 ) ^2 ) + 4
by A8, XREAL_1:8;
then
2
< sqrt (((x `2 ) ^2 ) + 4)
by SQUARE_1:85, SQUARE_1:95;
hence
x in {|[(- 1),0 ]|,|[1,0 ]|}
by A1, A2, A4, A9, Lm64, JORDAN24:def 1;
:: thesis: verum end; end; suppose A10:
x in LSeg |[1,3]|,
|[1,(- 3)]|
;
:: thesis: x in {|[(- 1),0 ]|,|[1,0 ]|}
|[1,(- 3)]| in LSeg |[1,(- 3)]|,
|[1,3]|
by RLTOPSP1:69;
then A11:
x `1 = 1
by A10, Lm32, Lm44, SPPOL_1:def 3;
per cases
( x `2 = 0 or x `2 <> 0 )
;
suppose
x `2 <> 0
;
:: thesis: x in {|[(- 1),0 ]|,|[1,0 ]|}then A12:
(x `2 ) ^2 > 0
by SQUARE_1:74;
A13:
dist x,
|[(- 1),0 ]| =
sqrt ((((x `1 ) - (|[(- 1),0 ]| `1 )) ^2 ) + (((x `2 ) - (|[(- 1),0 ]| `2 )) ^2 ))
by TOPREAL6:101
.=
sqrt (4 + ((x `2 ) ^2 ))
by A11, Lm18, Lm20
;
0 + 4
< ((x `2 ) ^2 ) + 4
by A12, XREAL_1:8;
then
2
< sqrt (((x `2 ) ^2 ) + 4)
by SQUARE_1:85, SQUARE_1:95;
hence
x in {|[(- 1),0 ]|,|[1,0 ]|}
by A1, A2, A4, A13, Lm64, JORDAN24:def 1;
:: thesis: verum end; end;
end;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {|[(- 1),0 ]|,|[1,0 ]|} or x in P /\ (rectangle (- 1),1,(- 3),3) )
assume
x in {|[(- 1),0 ]|,|[1,0 ]|}
; :: thesis: x in P /\ (rectangle (- 1),1,(- 3),3)
then A14:
( x = |[(- 1),0 ]| or x = |[1,0 ]| )
by TARSKI:def 2;
( |[(- 1),0 ]| in rectangle (- 1),1,(- 3),3 & |[1,0 ]| in rectangle (- 1),1,(- 3),3 )
by Lm18, Lm19, Lm20, Lm21, Lm59;
hence
x in P /\ (rectangle (- 1),1,(- 3),3)
by A2, A14, XBOOLE_0:def 4; :: thesis: verum