theorem Th3: :: LOPCLSET:3

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