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