theorem :: TEX_3:57

for X being non trivial TopSpace st ( for X0 being proper SubSpace of X holds not X0 is everywhere_dense ) holds
X is almost_discrete