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 set 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:69;
then A7: p `1 = |[(- 1),(- 3)]| `1 by A3, Lm46, SPPOL_1:def 3;
A8: |[(- 1),(- 3)]| `2 <= p `2 by A3, Lm29, JGRAPH_6:9;
A9: LSeg p,|[(- 1),(- 3)]| is vertical by A7, SPPOL_1:37;
p `2 <= |[(- 1),0 ]| `2 by A3, Lm20, JGRAPH_6:9;
then LSeg p,|[(- 1),(- 3)]| c= LSeg |[(- 1),(- 3)]|,|[(- 1),3]| by A7, A8, A9, Lm20, Lm27, Lm43, GOBOARD7:65;
then LSeg p,|[(- 1),(- 3)]| c= rectangle (- 1),1,(- 3),3 by Lm39, XBOOLE_1:1;
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:69;
then A11: |[(- 1),0 ]| `1 = p `1 by A3, Lm46, SPPOL_1:def 3;
A12: |[(- 1),0 ]| in C by A1, JORDAN24:def 1;
not p in C by A2, XBOOLE_0:def 5;
then |[(- 1),0 ]| `2 <> p `2 by A11, A12, TOPREAL3:11;
then A13: p `2 < |[(- 1),0 ]| `2 by A3, Lm20, JGRAPH_6:9;
p = |[(p `1 ),(p `2 )]| by EUCLID:57;
hence contradiction by A5, A7, A8, A10, A13, Lm19, Lm28, Lm34, JGRAPH_6:9; :: thesis: verum