let n be Element of NAT ; :: thesis: for A being Subset of (TOP-REAL n) holds UBD A is a_union_of_components of (TOP-REAL n) | (A ` )
let A be Subset of (TOP-REAL n); :: thesis: UBD A is a_union_of_components of (TOP-REAL n) | (A ` )
{ B where B is Subset of (TOP-REAL n) : B is_outside_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_outside_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_outside_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_outside_component_of A ) ;
ex C being Subset of ((TOP-REAL n) | (A ` )) st
( C = B & C is_a_component_of (TOP-REAL n) | (A ` ) & C is not bounded Subset of (Euclid n) ) by A1, Th18;
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_outside_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 ` )) ;
A2: UBD 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
A3: ( B = B0 & B is_outside_component_of A ) ;
ex C being Subset of ((TOP-REAL n) | (A ` )) st
( C = B & C is_a_component_of (TOP-REAL n) | (A ` ) & C is not bounded Subset of (Euclid n) ) by A3, Th18;
hence B0 is_a_component_of (TOP-REAL n) | (A ` ) by A3; :: thesis: verum

end;

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