let P be Subset of (TOP-REAL 2); :: thesis: ( |[(- 1),0]|,|[1,0]| realize-max-dist-in P implies P c= closed_inside_of_rectangle ((- 1),1,(- 3),3) )
assume that
A1: |[(- 1),0]| in P and
A2: |[1,0]| in P and
A3: for x, y being Point of (TOP-REAL 2) st x in P & y in P holds
dist (|[(- 1),0]|,|[1,0]|) >= dist (x,y) ; :: according to JORDAN24:def 1 :: thesis: P c= closed_inside_of_rectangle ((- 1),1,(- 3),3)
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in P or p in closed_inside_of_rectangle ((- 1),1,(- 3),3) )
assume A4: p in P ; :: thesis: p in closed_inside_of_rectangle ((- 1),1,(- 3),3)
then reconsider p = p as Point of (TOP-REAL 2) ;
A5: dist (|[(- 1),0]|,p) = sqrt ((((- 1) - (p `1)) ^2) + ((0 - (p `2)) ^2)) by Lm16, Lm18, TOPREAL6:92
.= sqrt ((((- 1) - (p `1)) ^2) + ((p `2) ^2)) ;
A6: now :: thesis: not 9 < (p `2) ^2
assume 9 < (p `2) ^2 ; :: thesis: contradiction
then 0 + 9 < (((- 1) - (p `1)) ^2) + ((p `2) ^2) by XREAL_1:8;
then 3 < sqrt ((((- 1) - (p `1)) ^2) + ((p `2) ^2)) by Lm65, SQUARE_1:27;
then 2 < sqrt ((((- 1) - (p `1)) ^2) + ((p `2) ^2)) by XXREAL_0:2;
hence contradiction by A1, A3, A4, A5, Lm66; :: thesis: verum
end;
A7: now :: thesis: not - 1 > p `1
assume A8: - 1 > p `1 ; :: thesis: contradiction
then LSeg (p,|[1,0]|) meets Vertical_Line (- 1) by Lm17, Th8;
then consider x being object such that
A9: x in LSeg (p,|[1,0]|) and
A10: x in Vertical_Line (- 1) by XBOOLE_0:3;
reconsider x = x as Point of (TOP-REAL 2) by A9;
A11: x `1 = - 1 by A10, JORDAN6:31;
A12: dist (p,|[1,0]|) = (dist (p,x)) + (dist (x,|[1,0]|)) by A9, JORDAN1K:29;
A13: dist (x,|[1,0]|) = sqrt ((((x `1) - (|[1,0]| `1)) ^2) + (((x `2) - (|[1,0]| `2)) ^2)) by TOPREAL6:92
.= sqrt (((- 2) ^2) + (((x `2) - 0) ^2)) by A11, Lm17, EUCLID:52
.= sqrt (4 + ((x `2) ^2)) ;
now :: thesis: not dist (x,|[1,0]|) < dist (|[(- 1),0]|,|[1,0]|)
assume dist (x,|[1,0]|) < dist (|[(- 1),0]|,|[1,0]|) ; :: thesis: contradiction
then 4 + ((x `2) ^2) < 4 + 0 by A13, Lm66, SQUARE_1:20, SQUARE_1:26;
hence contradiction by XREAL_1:6; :: thesis: verum
end;
then (dist (p,|[1,0]|)) + 0 > (dist (|[(- 1),0]|,|[1,0]|)) + 0 by A8, A11, A12, JORDAN1K:22, XREAL_1:8;
hence contradiction by A2, A3, A4; :: thesis: verum
end;
A14: now :: thesis: not p `1 > 1
assume A15: p `1 > 1 ; :: thesis: contradiction
then LSeg (p,|[(- 1),0]|) meets Vertical_Line 1 by Lm16, Th8;
then consider x being object such that
A16: x in LSeg (p,|[(- 1),0]|) and
A17: x in Vertical_Line 1 by XBOOLE_0:3;
reconsider x = x as Point of (TOP-REAL 2) by A16;
A18: x `1 = 1 by A17, JORDAN6:31;
A19: dist (p,|[(- 1),0]|) = (dist (p,x)) + (dist (x,|[(- 1),0]|)) by A16, JORDAN1K:29;
A20: 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 A18, Lm16, Lm18 ;
now :: thesis: not dist (x,|[(- 1),0]|) < dist (|[(- 1),0]|,|[1,0]|)
assume dist (x,|[(- 1),0]|) < dist (|[(- 1),0]|,|[1,0]|) ; :: thesis: contradiction
then 4 + ((x `2) ^2) < 4 + 0 by A20, Lm66, SQUARE_1:20, SQUARE_1:26;
hence contradiction by XREAL_1:6; :: thesis: verum
end;
then (dist (p,|[(- 1),0]|)) + 0 > (dist (|[(- 1),0]|,|[1,0]|)) + 0 by A15, A18, A19, JORDAN1K:22, XREAL_1:8;
hence contradiction by A1, A3, A4; :: thesis: verum
end;
A21: now :: thesis: not - 3 > p `2
assume - 3 > p `2 ; :: thesis: contradiction
then (p `2) ^2 > (- 3) ^2 by SQUARE_1:44;
hence contradiction by A6; :: thesis: verum
end;
3 >= p `2 by A6, Lm64, SQUARE_1:16;
hence p in closed_inside_of_rectangle ((- 1),1,(- 3),3) by A7, A14, A21; :: thesis: verum