let n be Element of 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 set ; :: 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 & B is_inside_component_of A ) ;
consider C being Subset of ((TOP-REAL n) | (A ` )) such that
A2: ( C = B & C is_a_component_of (TOP-REAL n) | (A ` ) & C is bounded Subset of (Euclid n) ) by A1, Th17;
thus x in bool the carrier of ((TOP-REAL n) | (A ` )) by A1, A2; :: 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: BDD A = union F0 ;
for B0 being Subset of ((TOP-REAL n) | (A ` )) st B0 in F0 holds
B0 is_a_component_of (TOP-REAL n) | (A ` )

proof

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

end;

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