for T being non empty TopSpace holds the carrier of (Closed_Domains_Lattice T) = Closed_Domains_of T