for X being TopStruct
for Y being SubSpace of X holds the carrier of Y c= the carrier of X