theorem Th31: :: PRE_TOPC:31

for T being TopSpace
for X being set holds
( X is closed Subset of T iff X is closed Subset of TopStruct(# the carrier of T, the topology of T #) )