take {} GX ; :: thesis: 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 )
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; :: thesis: verum