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)]| & Pf = f ) by Th43;
( |[(- 1),0 ]| = W-min C & |[1,0 ]| = E-max C ) by A1, Th79, Th80;
then Upper_Arc C is_an_arc_of |[(- 1),0 ]|,|[1,0 ]| by 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
A3: ( rng g = Upper_Arc C & Pg = g ) by Th42;
A4: Upper_Arc C c= C by JORDAN6:76;
A5: C c= closed_inside_of_rectangle (- 1),1,(- 3),3 by A1, Th71;
A6: ( |[(- 1),0 ]| in C & |[1,0 ]| in C ) by A1, JORDAN24:def 1;
A7: the carrier of (Trectangle (- 1),1,(- 3),3) = closed_inside_of_rectangle (- 1),1,(- 3),3 by PRE_TOPC:29;
reconsider AR = |[(- 1),0 ]|, BR = |[1,0 ]|, CR = |[0 ,3]|, DR = |[0 ,(- 3)]| as Point of (Trectangle (- 1),1,(- 3),3) by A5, A6, Lm60, Lm61, Lm65, PRE_TOPC:29;
rng Pg c= the carrier of (Trectangle (- 1),1,(- 3),3) by A3, A4, A5, A7, XBOOLE_1:1;
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 Lm60, Lm61, Lm65, JORDAN1:def 1;
then reconsider v = Pf as Path of CR,DR by A2, A7, Th30;
consider s, t being Point of I[01] such that
A8: h . s = v . t by Lm18, Lm19, Lm23, Lm25, JGRAPH_8:6;
( dom h = the carrier of I[01] & dom v = the carrier of I[01] ) by FUNCT_2:def 1;
then ( v . t in rng Pf & h . s in rng Pg ) by FUNCT_1:def 5;
hence LSeg |[0 ,3]|,|[0 ,(- 3)]| meets C by A2, A3, A4, A8, XBOOLE_0:3; :: thesis: verum