:: deftheorem Def1 defines Component_of CONNSP_3:def 1 :
for GX being TopStruct
for V, b₃ being Subset of GX holds
( b₃ = Component_of V iff ex F being Subset-Family of GX st
( ( for A being Subset of GX holds
( A in F iff ( A is connected & V c= A ) ) ) & union F = b₃ ) );