for T being non empty TopSpace holds Top (Open_setLatt T) = the carrier of T