theorem Th11: :: PRE_TOPC:11

for T being TopStruct
for X9 being SubSpace of T
for A being Subset of X9 holds A is Subset of T