theorem Th18: :: TDLAT_3:18

for X being TopSpace holds
( X is anti-discrete iff for A being Subset of X holds
( not A is open or A = {} or A = the carrier of X ) )