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