theorem :: TEX_4:79

for Y being non empty TopStruct
for A being non empty Subset of Y holds A is Subset of (Sspace A)