:: deftheorem defines almost_discrete TDLAT_3:def 3 :
for IT being TopStruct holds
( IT is almost_discrete iff for A being Subset of IT st A in the topology of IT holds
the carrier of IT \ A in the topology of IT );