:: deftheorem defines connected RCOMP_3:def 1 :
for T being TopStruct
for F being Subset-Family of T holds
( F is connected iff for X being Subset of T st X in F holds
X is connected );