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 by TOPS_1:def 3;
assume A = {} ; :: thesis: contradiction
then Cl A = {} X by PRE_TOPC:52;
hence contradiction by A1; :: thesis: verum