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:11;
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:22; :: 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 object ; :: 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