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
p `2 < 3
let P be Subset of (TOP-REAL 2); :: thesis: ( |[(- 1),0]|,|[1,0]| realize-max-dist-in P & p in P implies p `2 < 3 )
assume that
A1: |[(- 1),0]|,|[1,0]| realize-max-dist-in P and
A2: p in P ; :: thesis: p `2 < 3
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, Lm21, Lm24, Lm25, Lm28, Lm29, GOBOARD7:8;
then p in P /\ (rectangle ((- 1),1,(- 3),3)) by A2, Lm40, XBOOLE_0:def 4;
hence contradiction by A3, A5, Lm18, Lm19, Lm21, TARSKI:def 2; :: thesis: verum
end;
hence p `2 < 3 by A4, Lm21, XXREAL_0:1; :: thesis: verum