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