:: deftheorem defines anti-discrete TEX_4:def 1 :
for Y being TopStruct
for IT being Subset of Y holds
( IT is anti-discrete iff for x being Point of Y
for G being Subset of Y st G is open & x in G & x in IT holds
IT c= G );