theorem Th35: :: PRE_TOPC:35

for S, T being TopStruct holds
( S is SubSpace of T iff S is SubSpace of TopStruct(# the carrier of T, the topology of T #) )