for T being TopSpace holds [#] T is closed_condensed