:: deftheorem defines anti-discrete TEX_4:def 4 :
for Y being TopStruct
for A being Subset of Y holds
( A is anti-discrete iff for F being Subset of Y holds
( not F is closed or A misses F or A c= F ) );