theorem Th8: :: TMAP_1:8
for X, X1, X2 being TopSpace st X2 = TopStruct(# the carrier of X1, the topology of X1 #) holds
( X1 is closed SubSpace of X iff X2 is closed SubSpace of X )