theorem Th6: :: TMAP_1:6

for X being TopStruct
for X0 being SubSpace of X holds TopStruct(# the carrier of X0, the topology of X0 #) is strict SubSpace of X