theorem :: LOPCLSET:13

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