let P be Subset of (TOP-REAL 2); ( |[(- 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)
; JORDAN24:def 1 P c= closed_inside_of_rectangle ((- 1),1,(- 3),3)
let p be object ; TARSKI:def 3 ( not p in P or p in closed_inside_of_rectangle ((- 1),1,(- 3),3) )
assume A4:
p in P
; 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))
;
A7:
now not - 1 > p `1 assume A8:
- 1
> p `1
;
contradictionthen
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))
;
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;
verum end;
A14:
now not p `1 > 1assume A15:
p `1 > 1
;
contradictionthen
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
;
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;
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; verum