let P be Subset of (TOP-REAL 2); ( |[(- 1),0]|,|[1,0]| realize-max-dist-in P implies P misses LSeg (|[(- 1),(- 3)]|,|[1,(- 3)]|) )
assume A1:
|[(- 1),0]|,|[1,0]| realize-max-dist-in P
; P misses LSeg (|[(- 1),(- 3)]|,|[1,(- 3)]|)
assume
P meets LSeg (|[(- 1),(- 3)]|,|[1,(- 3)]|)
; contradiction
then consider x being object such that
A2:
x in P
and
A3:
x in LSeg (|[(- 1),(- 3)]|,|[1,(- 3)]|)
by XBOOLE_0:3;
reconsider x = x as Point of (TOP-REAL 2) by A2;
|[(- 1),(- 3)]| in LSeg (|[(- 1),(- 3)]|,|[1,(- 3)]|)
by RLTOPSP1:68;
then A4:
x `2 = - 3
by A3, Lm27, Lm56;
A5: dist (|[(- 1),0]|,x) =
sqrt ((((|[(- 1),0]| `1) - (x `1)) ^2) + (((|[(- 1),0]| `2) - (x `2)) ^2))
by TOPREAL6:92
.=
sqrt ((((- 1) - (x `1)) ^2) + ((- (- 3)) ^2))
by A4, Lm18, EUCLID:52
;
0 + 4 < (((- 1) - (x `1)) ^2) + 9
by XREAL_1:8;
then
2 < dist (|[(- 1),0]|,x)
by A5, SQUARE_1:20, SQUARE_1:27;
hence
contradiction
by A1, A2, Lm66; verum