for X being non empty TopSpace
for A being Subset of X st A is everywhere_dense & A is discrete holds
A is open