:: deftheorem Def2 defines a_union_of_components CONNSP_3:def 2 :
for GX being TopStruct
for b₂ being Subset of GX holds
( b₂ is a_union_of_components of GX iff ex F being Subset-Family of GX st
( ( for B being Subset of GX st B in F holds
B is a_component ) & b₂ = union F ) );