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