for Y being non empty TopStruct
for Y0 being non empty SubSpace of Y
for A being Subset of Y st A = the carrier of Y0 holds
( A is discrete iff Y0 is discrete )