for T being TopSpace holds Open_Domains_Lattice T is SubLattice of Domains_Lattice T