let C be Simple_closed_curve; :: thesis: ( |[(- 1),0]|,|[1,0]| realize-max-dist-in C implies LSeg (|[0,3]|,|[0,(- 3)]|) meets C )
assume A1: |[(- 1),0]|,|[1,0]| realize-max-dist-in C ; :: thesis: LSeg (|[0,3]|,|[0,(- 3)]|) meets C
set Jc = Upper_Arc C;
consider Pf being Path of |[0,3]|,|[0,(- 3)]|, f being Function of I[01],((TOP-REAL 2) | (LSeg (|[0,3]|,|[0,(- 3)]|))) such that
A2: rng f = LSeg (|[0,3]|,|[0,(- 3)]|) and
A3: Pf = f by Th43;
A4: |[(- 1),0]| = W-min C by A1, Th79;
|[1,0]| = E-max C by A1, Th80;
then Upper_Arc C is_an_arc_of |[(- 1),0]|,|[1,0]| by A4, JORDAN6:def 8;
then consider Pg being Path of |[(- 1),0]|,|[1,0]|, g being Function of I[01],((TOP-REAL 2) | (Upper_Arc C)) such that
A5: rng g = Upper_Arc C and
A6: Pg = g by Th42;
A7: Upper_Arc C c= C by JORDAN6:61;
A8: C c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by A1, Th71;
A9: |[(- 1),0]| in C by A1;
A10: |[1,0]| in C by A1;
A11: the carrier of (Trectangle ((- 1),1,(- 3),3)) = closed_inside_of_rectangle ((- 1),1,(- 3),3) by PRE_TOPC:8;
reconsider AR = |[(- 1),0]|, BR = |[1,0]|, CR = |[0,3]|, DR = |[0,(- 3)]| as Point of (Trectangle ((- 1),1,(- 3),3)) by A8, A9, A10, Lm62, Lm63, Lm67, PRE_TOPC:8;
rng Pg c= the carrier of (Trectangle ((- 1),1,(- 3),3)) by A5, A6, A7, A8, A11;
then reconsider h = Pg as Path of AR,BR by Th30;
LSeg (|[0,3]|,|[0,(- 3)]|) c= closed_inside_of_rectangle ((- 1),1,(- 3),3) by Lm62, Lm63, Lm67, JORDAN1:def 1;
then reconsider v = Pf as Path of CR,DR by A2, A3, A11, Th30;
consider s, t being Point of I[01] such that
A12: h . s = v . t by Lm16, Lm17, Lm21, Lm23, JGRAPH_8:6;
A13: dom h = the carrier of I[01] by FUNCT_2:def 1;
dom v = the carrier of I[01] by FUNCT_2:def 1;
then A14: v . t in rng Pf by FUNCT_1:def 3;
h . s in rng Pg by A13, FUNCT_1:def 3;
hence LSeg (|[0,3]|,|[0,(- 3)]|) meets C by A2, A3, A5, A6, A7, A12, A14, XBOOLE_0:3; :: thesis: verum