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, Lm56, 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