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, 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; :: thesis: verum