theorem Th1: :: BORSUK_1:1
for X being TopStruct
for Y being SubSpace of X holds the carrier of Y c= the carrier of X