:: deftheorem defines Open_Domains_Lattice TDLAT_1:def 12 :
for T being TopSpace holds Open_Domains_Lattice T = LattStr(# (Open_Domains_of T),(Open_Domains_Union T),(Open_Domains_Meet T) #);