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