:: deftheorem defines Open_Domains_of TDLAT_1:def 9 :
for T being TopStruct holds Open_Domains_of T = { A where A is Subset of T : A is open_condensed } ;