:: deftheorem defines anti-discrete TEX_4:def 2 :
for Y being non empty TopStruct
for A being Subset of Y holds
( A is anti-discrete iff for x being Point of Y
for F being Subset of Y st F is closed & x in F & x in A holds
A c= F );