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 set ; :: 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:101
.= sqrt ((((- 1) - (p `1 )) ^2 ) + ((p `2 ) ^2 )) ;

A6: now

assume 9 < (p `2 ) ^2 ; :: thesis: contradiction
then 0 + 9 < (((- 1) - (p `1 )) ^2 ) + ((p `2 ) ^2 ) by XREAL_1:10;
then 3 < sqrt ((((- 1) - (p `1 )) ^2 ) + ((p `2 ) ^2 )) by Lm65, SQUARE_1:95;
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

assume A8: - 1 > p `1 ; :: thesis: contradiction
then LSeg p,|[1,0 ]| meets Vertical_Line (- 1) by Lm17, Th8;
then consider x being set 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:34;
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:101
.= sqrt (((- 2) ^2 ) + (((x `2 ) - 0 ) ^2 )) by A11, Lm17, EUCLID:56
.= sqrt (4 + ((x `2 ) ^2 )) ;

now

assume dist x,|[1,0 ]| < dist |[(- 1),0 ]|,|[1,0 ]| ; :: thesis: contradiction
then 4 + ((x `2 ) ^2 ) < 4 + 0 by A13, Lm66, SQUARE_1:85, SQUARE_1:94;
hence contradiction by XREAL_1:8; :: thesis: verum

end;

then (dist p,|[1,0 ]|) + 0 > (dist |[(- 1),0 ]|,|[1,0 ]|) + 0 by A8, A11, A12, JORDAN1K:22, XREAL_1:10;
hence contradiction by A2, A3, A4; :: thesis: verum

end;

A14: now

assume A15: p `1 > 1 ; :: thesis: contradiction
then LSeg p,|[(- 1),0 ]| meets Vertical_Line 1 by Lm16, Th8;
then consider x being set 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:34;
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:101
.= sqrt (4 + ((x `2 ) ^2 )) by A18, Lm16, Lm18 ;

now

assume dist x,|[(- 1),0 ]| < dist |[(- 1),0 ]|,|[1,0 ]| ; :: thesis: contradiction
then 4 + ((x `2 ) ^2 ) < 4 + 0 by A20, Lm66, SQUARE_1:85, SQUARE_1:94;
hence contradiction by XREAL_1:8; :: thesis: verum

end;

then (dist p,|[(- 1),0 ]|) + 0 > (dist |[(- 1),0 ]|,|[1,0 ]|) + 0 by A15, A18, A19, JORDAN1K:22, XREAL_1:10;
hence contradiction by A1, A3, A4; :: thesis: verum

end;

A21: now

assume - 3 > p `2 ; :: thesis: contradiction
then (p `2 ) ^2 > (- 3) ^2 by SQUARE_1:114;
hence contradiction by A6; :: thesis: verum

end;

3 >= p `2 by A6, Lm64, SQUARE_1:78;
hence p in closed_inside_of_rectangle (- 1),1,(- 3),3 by A7, A14, A21; :: thesis: verum