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 ;
A3: |[1,0]| in P by A1;
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 object ; :: 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:68;
then A8: x `1 = - 1 by A7, Lm26, Lm45;
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:12;
A10: dist (|[1,0]|,x) = sqrt (((1 - (- 1)) ^2) + ((0 - (x `2)) ^2)) by A8, Lm17, Lm19, TOPREAL6:92
.= sqrt (4 + ((x `2) ^2)) ;
0 + 4 < ((x `2) ^2) + 4 by A9, XREAL_1:6;
then 2 < sqrt (((x `2) ^2) + 4) by SQUARE_1:20, SQUARE_1:27;
hence x in {|[(- 1),0]|,|[1,0]|} by A1, A5, A10, Lm66; :: 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:68;
then A12: x `1 = 1 by A11, Lm30, Lm46;
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:12;
A14: dist (x,|[(- 1),0]|) = sqrt ((((x `1) - (|[(- 1),0]| `1)) ^2) + (((x `2) - (|[(- 1),0]| `2)) ^2)) by TOPREAL6:92
.= sqrt (4 + ((x `2) ^2)) by A12, Lm16, Lm18 ;
0 + 4 < ((x `2) ^2) + 4 by A13, XREAL_1:6;
then 2 < sqrt (((x `2) ^2) + 4) by SQUARE_1:20, SQUARE_1:27;
hence x in {|[(- 1),0]|,|[1,0]|} by A1, A5, A14, Lm66; :: 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 object ; :: 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