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