let C be Simple_closed_curve; :: thesis: ( |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in C implies for 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 holds
BDD C = Component_of (Down ((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))),(C ` )) )
assume A1: |[(- 1),0 ]|,|[1,0 ]| realize-max-dist-in C ; :: thesis: for 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 holds
BDD C = Component_of (Down ((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))),(C ` ))
let Jc, Jd be compact with_the_max_arc Subset of (TOP-REAL 2); :: thesis: ( 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 implies BDD C = Component_of (Down ((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))),(C ` )) )
assume that
A2: Jc is_an_arc_of |[(- 1),0 ]|,|[1,0 ]| and
A3: Jd is_an_arc_of |[(- 1),0 ]|,|[1,0 ]| and
A4: C = Jc \/ Jd and
A5: Jc /\ Jd = {|[(- 1),0 ]|,|[1,0 ]|} and
A6: UMP C in Jc and
A7: LMP C in Jd and
A8: W-bound C = W-bound Jc and
A9: E-bound C = E-bound Jc ; :: thesis: BDD C = Component_of (Down ((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))),(C ` ))
reconsider Ux = Component_of (Down ((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))),(C ` )) as Subset of (TOP-REAL 2) by PRE_TOPC:39;
Ux = BDD C

proof

Ux is_inside_component_of C by A1, A2, A3, A4, A5, A6, A7, A8, A9, Th95;
hence Ux c= BDD C by JORDAN2C:26; :: according to XBOOLE_0:def 10 :: thesis: BDD C c= Ux
set F = { B where B is Subset of (TOP-REAL 2) : B is_inside_component_of C } ;
let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in BDD C or q in Ux )
assume q in BDD C ; :: thesis: q in Ux
then consider Z being set such that
A10: q in Z and
A11: Z in { B where B is Subset of (TOP-REAL 2) : B is_inside_component_of C } by TARSKI:def 4;
ex B being Subset of (TOP-REAL 2) st
( Z = B & B is_inside_component_of C ) by A11;
hence q in Ux by A1, A2, A3, A4, A5, A6, A7, A8, A9, A10, Th95; :: thesis: verum

end;

hence BDD C = Component_of (Down ((1 / 2) * ((UMP ((LSeg (LMP Jc),|[0 ,(- 3)]|) /\ Jd)) + (LMP Jc))),(C ` )) ; :: thesis: verum