let X be non empty TopSpace; :: thesis: for A being Subset of X st A is dense holds
A <> {}
let A be Subset of X; :: thesis: ( A is dense implies A <> {} )
assume A is dense ; :: thesis: A <> {}
then A1: Cl A = [#] X ;
assume A = {} ; :: thesis: contradiction
hence contradiction by A1, PRE_TOPC:22; :: thesis: verum