let T be non empty TopSpace; :: thesis: the carrier of (Closed_Domains_Lattice T) = Closed_Domains_of T
Closed_Domains_Lattice T = LattStr(# (Closed_Domains_of T),(CLD-Union T),(CLD-Meet T) #) by TDLAT_1:def 8;
hence the carrier of (Closed_Domains_Lattice T) = Closed_Domains_of T ; :: thesis: verum