let p be Point of (TOP-REAL 2); for C being Simple_closed_curve st |[(- 1),0]|,|[1,0]| realize-max-dist-in C & p in C ` & p in LSeg (|[1,0]|,|[1,(- 3)]|) holds
LSeg (p,|[1,(- 3)]|) misses C
let C be Simple_closed_curve; ( |[(- 1),0]|,|[1,0]| realize-max-dist-in C & p in C ` & p in LSeg (|[1,0]|,|[1,(- 3)]|) implies LSeg (p,|[1,(- 3)]|) misses C )
assume that
A1:
|[(- 1),0]|,|[1,0]| realize-max-dist-in C
and
A2:
p in C `
and
A3:
p in LSeg (|[1,0]|,|[1,(- 3)]|)
; LSeg (p,|[1,(- 3)]|) misses C
A4:
C /\ (rectangle ((- 1),1,(- 3),3)) = {|[(- 1),0]|,|[1,0]|}
by A1, Th74;
assume
LSeg (p,|[1,(- 3)]|) meets C
; contradiction
then consider q being object such that
A5:
q in LSeg (p,|[1,(- 3)]|)
and
A6:
q in C
by XBOOLE_0:3;
reconsider q = q as Point of (TOP-REAL 2) by A6;
|[1,(- 3)]| in LSeg (|[1,0]|,|[1,(- 3)]|)
by RLTOPSP1:68;
then A7:
p `1 = |[1,(- 3)]| `1
by A3, Lm50;
A8:
|[1,(- 3)]| `2 <= p `2
by A3, Lm31, JGRAPH_6:1;
A9:
LSeg (p,|[1,(- 3)]|) is vertical
by A7, SPPOL_1:16;
p `2 <= |[1,0]| `2
by A3, Lm19, JGRAPH_6:1;
then
LSeg (p,|[1,(- 3)]|) c= LSeg (|[1,(- 3)]|,|[1,3]|)
by A7, A8, A9, Lm19, Lm29, Lm46, GOBOARD7:63;
then
LSeg (p,|[1,(- 3)]|) c= rectangle ((- 1),1,(- 3),3)
by Lm42;
then
q in (rectangle ((- 1),1,(- 3),3)) /\ C
by A5, A6, XBOOLE_0:def 4;
then A10:
( q = |[(- 1),0]| or q = |[1,0]| )
by A4, TARSKI:def 2;
|[1,0]| in LSeg (|[1,0]|,|[1,(- 3)]|)
by RLTOPSP1:68;
then A11:
|[1,0]| `1 = p `1
by A3, Lm50;
A12:
|[1,0]| in C
by A1;
not p in C
by A2, XBOOLE_0:def 5;
then
|[1,0]| `2 <> p `2
by A11, A12, TOPREAL3:6;
then A13:
p `2 < |[1,0]| `2
by A3, Lm19, JGRAPH_6:1;
p = |[(p `1),(p `2)]|
by EUCLID:53;
hence
contradiction
by A5, A7, A8, A10, A13, Lm16, Lm30, Lm34, JGRAPH_6:1; verum