for Y being non empty TopStruct
for Y0 being SubSpace of Y
for A being non empty Subset of Y st A is Subset of Y0 holds
Sspace A is SubSpace of Y0