:: deftheorem Def7 defines Component_of CONNSP_3:def 7 :
for GX being TopStruct
for B being Subset of GX
for p being Point of GX st p in B holds
for b₄ being Subset of GX holds
( b₄ = Component_of (p,B) iff for q being Point of (GX | B) st q = p holds
b₄ = Component_of q );