theorem :: LOPCLSET:14

for T being non empty TopSpace holds {} T is Element of (OpenClosedSetLatt T) by Th3;