for Y being non empty extremally_disconnected TopSpace holds Domains_Lattice Y = Closed_Domains_Lattice Y