:: deftheorem Def7 defines qComponent_of CONNSP_2:def 7 :
for X being non empty TopSpace
for x being Point of X
for b₃ being Subset of X holds
( b₃ = qComponent_of x iff ex F being Subset-Family of X st
( ( for A being Subset of X holds
( A in F iff ( A is open & A is closed & x in A ) ) ) & meet F = b₃ ) );