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, Lm49;
A8: p `2 <= |[1,3]| `2 by A3, Lm29, JGRAPH_6:1;
A9: LSeg (p,|[1,3]|) is vertical by A7, SPPOL_1:16;
|[1,0]| `2 <= p `2 by A3, Lm19, JGRAPH_6:1;
then LSeg (p,|[1,3]|) c= LSeg (|[1,(- 3)]|,|[1,3]|) by A7, A8, A9, Lm19, Lm28, Lm30, Lm31, 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, Lm49;
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: |[1,0]| `2 < p `2 by A3, Lm19, JGRAPH_6:1;
p = |[(p `1),(p `2)]| by EUCLID:53;
hence contradiction by A5, A7, A8, A10, A13, Lm16, Lm28, Lm35, JGRAPH_6:1; :: thesis: verum