let p be Point of (TOP-REAL 2); :: thesis: for P being Subset of (TOP-REAL 2) st |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in P & p in P holds
- 3 < p `2
let P be Subset of (TOP-REAL 2); :: thesis: ( |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in P & p in P implies - 3 < p `2 )
assume that
A1: |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in P and
A2: p in P ; :: thesis: - 3 < p `2
A3: P /\ (rectangle (- 1),1,(- 3),3) = {|[(- 1),0 ]|,|[1,0 ]|} by A1, Th74;
P c= closed_inside_of_rectangle (- 1),1,(- 3),3 by A1, Th71;
then p in closed_inside_of_rectangle (- 1),1,(- 3),3 by A2;
then A4: ex p1 being Point of (TOP-REAL 2) st
( p1 = p & - 1 <= p1 `1 & p1 `1 <= 1 & - 3 <= p1 `2 & p1 `2 <= 3 ) ;

now

assume A5: p `2 = |[0 ,(- 3)]| `2 ; :: thesis: contradiction
then p in LSeg |[(- 1),(- 3)]|,|[1,(- 3)]| by A4, Lm25, Lm28, Lm29, Lm32, Lm33, GOBOARD7:9;
then p in P /\ (rectangle (- 1),1,(- 3),3) by A2, Lm42, XBOOLE_0:def 4;
then ( p = |[(- 1),0 ]| or p = |[1,0 ]| ) by A3, TARSKI:def 2;
hence contradiction by A5, Lm25, EUCLID:56; :: thesis: verum

end;

hence - 3 < p `2 by A4, Lm25, XXREAL_0:1; :: thesis: verum