theorem Th9: :: TSP_1:9

for Y being non empty TopStruct
for A being Subset of Y st A is discrete holds
A is T_0