for Y being non empty TopStruct
for Y0 being SubSpace of Y
for A being Subset of Y st A = the carrier of Y0 & Y0 is anti-discrete holds
A is anti-discrete