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, Lm48, SPPOL_1:def 3;
A8: |[1,(- 3)]| `2 <= p `2 by A3, Lm33, JGRAPH_6:9;
A9: LSeg p,|[1,(- 3)]| is vertical by A7, SPPOL_1:37;
p `2 <= |[1,0 ]| `2 by A3, Lm21, JGRAPH_6:9;
then LSeg p,|[1,(- 3)]| c= LSeg |[1,(- 3)]|,|[1,3]| by A7, A8, A9, Lm21, Lm31, Lm44, GOBOARD7:65;
then LSeg p,|[1,(- 3)]| c= rectangle (- 1),1,(- 3),3 by Lm41, 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, Lm48, 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, Lm21, JGRAPH_6:9;
p = |[(p `1 ),(p `2 )]| by EUCLID:57;
hence contradiction by A5, A7, A8, A10, A13, Lm18, Lm32, Lm36, JGRAPH_6:9; :: thesis: verum