:: deftheorem defines Domains_of TDLAT_1:def 1 :
for T being TopStruct holds Domains_of T = { A where A is Subset of T : A is condensed } ;