let n be Nat; :: thesis: for A being Subset of (TOP-REAL n) holds BDD A is a_union_of_components of (TOP-REAL n) | (A `)
let A be Subset of (TOP-REAL n); :: thesis: BDD A is a_union_of_components of (TOP-REAL n) | (A `)
{ B where B is Subset of (TOP-REAL n) : B is_inside_component_of A } c= bool the carrier of ((TOP-REAL n) | (A `))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { B where B is Subset of (TOP-REAL n) : B is_inside_component_of A } or x in bool the carrier of ((TOP-REAL n) | (A `)) )
assume x in { B where B is Subset of (TOP-REAL n) : B is_inside_component_of A } ; :: thesis: x in bool the carrier of ((TOP-REAL n) | (A `))
then consider B being Subset of (TOP-REAL n) such that
A1: x = B and
A2: B is_inside_component_of A ;
ex C being Subset of ((TOP-REAL n) | (A `)) st
( C = B & C is a_component & C is bounded Subset of (Euclid n) ) by A2, Th7;
hence x in bool the carrier of ((TOP-REAL n) | (A `)) by A1; :: thesis: verum

end;

then reconsider F0 = { B where B is Subset of (TOP-REAL n) : B is_inside_component_of A } as Subset-Family of the carrier of ((TOP-REAL n) | (A `)) ;
reconsider F0 = F0 as Subset-Family of ((TOP-REAL n) | (A `)) ;
A3: for B0 being Subset of ((TOP-REAL n) | (A `)) st B0 in F0 holds
B0 is a_component

proof

let B0 be Subset of ((TOP-REAL n) | (A `)); :: thesis: ( B0 in F0 implies B0 is a_component )
assume B0 in F0 ; :: thesis: B0 is a_component
then consider B being Subset of (TOP-REAL n) such that
A4: B = B0 and
A5: B is_inside_component_of A ;
ex C being Subset of ((TOP-REAL n) | (A `)) st
( C = B & C is a_component & C is bounded Subset of (Euclid n) ) by A5, Th7;
hence B0 is a_component by A4; :: thesis: verum

end;

BDD A = union F0 ;
hence BDD A is a_union_of_components of (TOP-REAL n) | (A `) by A3, CONNSP_3:def 2; :: thesis: verum