let T be non empty TopSpace; :: thesis: the carrier of (Open_Domains_Lattice T) = Open_Domains_of T
Open_Domains_Lattice T = LattStr(# (Open_Domains_of T),(OPD-Union T),(OPD-Meet T) #) by TDLAT_1:def 12;
hence the carrier of (Open_Domains_Lattice T) = Open_Domains_of T ; :: thesis: verum