theorem :: TEX_3:60

for X being non empty TopSpace st ex X0 being non empty SubSpace of X st
( X0 is everywhere_dense & X0 is proper ) holds
not X is almost_discrete ;