theorem Th8: :: PRE_TOPC:8

for GX being TopStruct
for A being Subset of GX holds the carrier of (GX | A) = A