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