let C be Simple_closed_curve; :: thesis: ( |[(- 1),0]|,|[1,0]| realize-max-dist-in C implies ex Jc, Jd being compact with_the_max_arc Subset of (TOP-REAL 2) st
( Jc is_an_arc_of |[(- 1),0]|,|[1,0]| & Jd is_an_arc_of |[(- 1),0]|,|[1,0]| & C = Jc \/ Jd & Jc /\ Jd = {|[(- 1),0]|,|[1,0]|} & UMP C in Jc & LMP C in Jd & W-bound C = W-bound Jc & E-bound C = E-bound Jc ) )
assume A1: |[(- 1),0]|,|[1,0]| realize-max-dist-in C ; :: thesis: ex Jc, Jd being compact with_the_max_arc Subset of (TOP-REAL 2) st
( Jc is_an_arc_of |[(- 1),0]|,|[1,0]| & Jd is_an_arc_of |[(- 1),0]|,|[1,0]| & C = Jc \/ Jd & Jc /\ Jd = {|[(- 1),0]|,|[1,0]|} & UMP C in Jc & LMP C in Jd & W-bound C = W-bound Jc & E-bound C = E-bound Jc )
set U = Upper_Arc C;
set L = Lower_Arc C;
A2: (Upper_Arc C) \/ (Lower_Arc C) = C by JORDAN6:def 9;
A3: UMP C in C by JORDAN21:30;
LMP C in C by JORDAN21:31;
then A4: ( LMP C in Upper_Arc C or LMP C in Lower_Arc C ) by A2, XBOOLE_0:def 3;
A5: W-min C = |[(- 1),0]| by A1, Th79;
A6: E-max C = |[1,0]| by A1, Th80;