theorem Th1: :: TSEP_1:1
for X being TopStruct
for X0 being SubSpace of X holds the carrier of X0 is Subset of X