:: deftheorem Def2 defines anti-discrete TDLAT_3:def 2 :
for IT being TopStruct holds
( IT is anti-discrete iff the topology of IT = {{}, the carrier of IT} );