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, Lm47;
A8: p `2 <= |[(- 1),3]| `2 by A3, Lm25, JGRAPH_6:1;
A9: LSeg (p,|[(- 1),3]|) is vertical by A7, SPPOL_1:16;
|[(- 1),0]| `2 <= p `2 by A3, Lm18, JGRAPH_6:1;
then LSeg (p,|[(- 1),3]|) c= LSeg (|[(- 1),(- 3)]|,|[(- 1),3]|) by A7, A8, A9, Lm18, Lm24, Lm26, Lm27, Lm45, GOBOARD7:63;
then LSeg (p,|[(- 1),3]|) c= rectangle ((- 1),1,(- 3),3) by Lm38;
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, Lm47;
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, Lm18, JGRAPH_6:1;
p = |[(p `1),(p `2)]| by EUCLID:53;
hence contradiction by A5, A7, A8, A10, A13, Lm17, Lm24, Lm33, JGRAPH_6:1; :: thesis: verum