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, Lm27, Lm53, 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, Lm20, 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, Lm64, JORDAN24:def 1; :: thesis: verum