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 by JORDAN24:def 1;
A3: |[1,0 ]| in P by A1, 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 A4: x in P /\ (rectangle (- 1),1,(- 3),3) ; :: thesis: x in {|[(- 1),0 ]|,|[1,0 ]|}
then A5: x in P by XBOOLE_0:def 4;
x in rectangle (- 1),1,(- 3),3 by A4, XBOOLE_0:def 4;
then A6: ( 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 Lm36, XBOOLE_0:def 3;
reconsider x = x as Point of (TOP-REAL 2) by A4;
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 A6, XBOOLE_0:def 3;
suppose A7: 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 A8: x `1 = - 1 by A7, Lm26, Lm45, 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 A9: (x `2 ) ^2 > 0 by SQUARE_1:74;
A10: dist |[1,0 ]|,x = sqrt (((1 - (- 1)) ^2 ) + ((0 - (x `2 )) ^2 )) by A8, Lm17, Lm19, TOPREAL6:101
.= sqrt (4 + ((x `2 ) ^2 )) ;
0 + 4 < ((x `2 ) ^2 ) + 4 by A9, 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, A3, A5, A10, Lm66, JORDAN24:def 1; :: thesis: verum
end;
end;
end;
suppose A11: 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 A12: x `1 = 1 by A11, Lm30, Lm46, 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 A13: (x `2 ) ^2 > 0 by SQUARE_1:74;
A14: 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 A12, Lm16, Lm18 ;
0 + 4 < ((x `2 ) ^2 ) + 4 by A13, 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, A5, A14, Lm66, JORDAN24:def 1; :: thesis: verum
end;
end;
end;
suppose x in LSeg |[1,(- 3)]|,|[(- 1),(- 3)]| ; :: thesis: x in {|[(- 1),0 ]|,|[1,0 ]|}
then LSeg |[1,(- 3)]|,|[(- 1),(- 3)]| meets P by A5, XBOOLE_0:3;
hence x in {|[(- 1),0 ]|,|[1,0 ]|} by A1, Th73; :: 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 A15: ( x = |[(- 1),0 ]| or x = |[1,0 ]| ) by TARSKI:def 2;
A16: |[(- 1),0 ]| in rectangle (- 1),1,(- 3),3 by Lm16, Lm18, Lm61;
|[1,0 ]| in rectangle (- 1),1,(- 3),3 by Lm17, Lm19, Lm61;
hence x in P /\ (rectangle (- 1),1,(- 3),3) by A2, A3, A15, A16, XBOOLE_0:def 4; :: thesis: verum