:: deftheorem defines Closed_Domains_of TDLAT_1:def 5 :
for T being TopStruct holds Closed_Domains_of T = { A where A is Subset of T : A is closed_condensed } ;