theorem Th1: :: LOPCLSET:1

for T being non empty TopSpace
for X being Subset of T st X in OpenClosedSet T holds
X is open