:: deftheorem Def1 defines discrete TDLAT_3:def 1 :
for IT being TopStruct holds
( IT is discrete iff the topology of IT = bool the carrier of IT );