for T being non empty TopSpace holds [#] T is Element of OpenClosedSet T by Th3;