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 :: thesis: not p `2 = |[0,(- 3)]| `2

assume A5: p `2 = |[0,(- 3)]| `2 ; :: thesis: contradiction
then p in LSeg (|[(- 1),(- 3)]|,|[1,(- 3)]|) by A4, Lm23, Lm26, Lm27, Lm30, Lm31, GOBOARD7:8;
then p in P /\ (rectangle ((- 1),1,(- 3),3)) by A2, Lm44, XBOOLE_0:def 4;
then ( p = |[(- 1),0]| or p = |[1,0]| ) by A3, TARSKI:def 2;
hence contradiction by A5, Lm23, EUCLID:52; :: thesis: verum

end;

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