let p be Point of (TOP-REAL 2); :: thesis: 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; :: thesis: ( |[(- 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)]|) ; :: thesis: 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 ; :: thesis: 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; :: thesis: verum