theorem :: TEX_1:34

for X being non empty TopSpace holds
( not X is almost_discrete iff ex A being Subset of X st
( A <> the carrier of X & A is dense & A is open ) )