theorem :: LOPCLSET:6

for T being non empty TopSpace holds {} T is Element of OpenClosedSet T by Th3;