theorem :: TEX_3:58

for X being non empty TopSpace st ex X0 being non empty SubSpace of X st X0 is nowhere_dense holds
not X is almost_discrete ;