:: deftheorem Def7 defines Component_of CONNSP_1:def 7 :
for GX being TopStruct
for x being Point of GX
for b₃ being Subset of GX holds
( b₃ = Component_of x iff ex F being Subset-Family of GX st
( ( for A being Subset of GX holds
( A in F iff ( A is connected & x in A ) ) ) & union F = b₃ ) );