let GX be non empty TopSpace; :: thesis: {} GX is a_union_of_components of GX
thus ex F being Subset-Family of st
( ( for B being Subset of st B in F holds
B is_a_component_of GX ) & {} GX = union F ) by Lm1; :: according to CONNSP_3:def 2 :: thesis: verum