:: deftheorem defines anti-discrete-set-family TEX_4:def 5 :
for Y being TopStruct
for IT being Subset-Family of Y holds
( IT is anti-discrete-set-family iff for A being Subset of Y st A in IT holds
A is anti-discrete );