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 set 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:69;
then A4: x `2 = 3 by A3, Lm25, Lm55, SPPOL_1:def 2;
A5: |[(- 1),0]| in P by A1, JORDAN24:def 1;
A6: dist (|[(- 1),0]|,x) = sqrt ((((|[(- 1),0]| `1) - (x `1)) ^2) + (((|[(- 1),0]| `2) - (x `2)) ^2)) by TOPREAL6:101
.= sqrt ((((- 1) - (x `1)) ^2) + (3 ^2)) by A4, Lm18, EUCLID:56 ;
0 + 4 < (((- 1) - (x `1)) ^2) + 9 by XREAL_1:10;
then 2 < dist (|[(- 1),0]|,x) by A6, SQUARE_1:85, SQUARE_1:95;
hence contradiction by A1, A2, A5, Lm66, JORDAN24:def 1; :: thesis: verum