let P be Subset of (TOP-REAL 2); :: thesis: ( |[(- 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 ; :: thesis: P misses LSeg (|[(- 1),3]|,|[1,3]|)
assume P meets LSeg (|[(- 1),3]|,|[1,3]|) ; :: thesis: 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, Lm25, Lm55;
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; :: thesis: verum