let T be non empty TopSpace; :: thesis: the carrier of (Domains_Lattice T) = Domains_of T
Domains_Lattice T = LattStr(# (Domains_of T),(D-Union T),(D-Meet T) #) by TDLAT_1:def 4;
hence the carrier of (Domains_Lattice T) = Domains_of T ; :: thesis: verum