let p be Point of (TOP-REAL 2); 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); ( |[(- 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
; - 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 not p `2 = |[0,(- 3)]| `2 assume A5:
p `2 = |[0,(- 3)]| `2
;
contradictionthen
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;
verum end;
hence
- 3 < p `2
by A4, Lm23, XXREAL_0:1; verum