theorem Th9: :: FINTOPO6:10

for FT being non empty RelStr
for X9 being SubSpace of FT
for A being Subset of X9 holds A is Subset of FT