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;

per cases ( UMP C in Upper_Arc C or UMP C in Lower_Arc C ) by A2, A3, XBOOLE_0:def 3;

suppose A7: UMP C in Upper_Arc 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 )

take Upper_Arc C ; :: thesis: ex Jd being compact with_the_max_arc Subset of (TOP-REAL 2) st
( Upper_Arc C is_an_arc_of |[(- 1),0]|,|[1,0]| & Jd is_an_arc_of |[(- 1),0]|,|[1,0]| & C = (Upper_Arc C) \/ Jd & (Upper_Arc C) /\ Jd = {|[(- 1),0]|,|[1,0]|} & UMP C in Upper_Arc C & LMP C in Jd & W-bound C = W-bound (Upper_Arc C) & E-bound C = E-bound (Upper_Arc C) )
take Lower_Arc C ; :: thesis: ( Upper_Arc C is_an_arc_of |[(- 1),0]|,|[1,0]| & Lower_Arc C is_an_arc_of |[(- 1),0]|,|[1,0]| & C = (Upper_Arc C) \/ (Lower_Arc C) & (Upper_Arc C) /\ (Lower_Arc C) = {|[(- 1),0]|,|[1,0]|} & UMP C in Upper_Arc C & LMP C in Lower_Arc C & W-bound C = W-bound (Upper_Arc C) & E-bound C = E-bound (Upper_Arc C) )
thus ( Upper_Arc C is_an_arc_of |[(- 1),0]|,|[1,0]| & Lower_Arc C is_an_arc_of |[(- 1),0]|,|[1,0]| & C = (Upper_Arc C) \/ (Lower_Arc C) & (Upper_Arc C) /\ (Lower_Arc C) = {|[(- 1),0]|,|[1,0]|} & UMP C in Upper_Arc C & LMP C in Lower_Arc C & W-bound C = W-bound (Upper_Arc C) & E-bound C = E-bound (Upper_Arc C) ) by A4, A5, A6, A7, JORDAN21:17, JORDAN21:18, JORDAN21:50, JORDAN6:50; :: thesis: verum

end;

suppose A8: UMP C in Lower_Arc 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 )

take Lower_Arc C ; :: thesis: ex Jd being compact with_the_max_arc Subset of (TOP-REAL 2) st
( Lower_Arc C is_an_arc_of |[(- 1),0]|,|[1,0]| & Jd is_an_arc_of |[(- 1),0]|,|[1,0]| & C = (Lower_Arc C) \/ Jd & (Lower_Arc C) /\ Jd = {|[(- 1),0]|,|[1,0]|} & UMP C in Lower_Arc C & LMP C in Jd & W-bound C = W-bound (Lower_Arc C) & E-bound C = E-bound (Lower_Arc C) )
take Upper_Arc C ; :: thesis: ( Lower_Arc C is_an_arc_of |[(- 1),0]|,|[1,0]| & Upper_Arc C is_an_arc_of |[(- 1),0]|,|[1,0]| & C = (Lower_Arc C) \/ (Upper_Arc C) & (Lower_Arc C) /\ (Upper_Arc C) = {|[(- 1),0]|,|[1,0]|} & UMP C in Lower_Arc C & LMP C in Upper_Arc C & W-bound C = W-bound (Lower_Arc C) & E-bound C = E-bound (Lower_Arc C) )
thus ( Lower_Arc C is_an_arc_of |[(- 1),0]|,|[1,0]| & Upper_Arc C is_an_arc_of |[(- 1),0]|,|[1,0]| & C = (Lower_Arc C) \/ (Upper_Arc C) & (Lower_Arc C) /\ (Upper_Arc C) = {|[(- 1),0]|,|[1,0]|} & UMP C in Lower_Arc C & LMP C in Upper_Arc C & W-bound C = W-bound (Lower_Arc C) & E-bound C = E-bound (Lower_Arc C) ) by A4, A5, A6, A8, JORDAN21:19, JORDAN21:20, JORDAN21:49, JORDAN6:50; :: thesis: verum

end;

end;