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:43;
LMP C in C
by JORDAN21:44;
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 ]| & E-max C = |[1,0 ]| )
by A1, Th79, Th80;
per cases
( UMP C in Upper_Arc C or UMP C in Lower_Arc C )
by A2, A3, XBOOLE_0:def 3;
suppose A6:
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, JORDAN21:26, JORDAN21:27, JORDAN21:63, JORDAN6:65;
:: thesis: verum end; suppose A7:
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, A7, JORDAN21:28, JORDAN21:29, JORDAN21:62, JORDAN6:65;
:: thesis: verum end;