let X be RealNormSpace; :: thesis: for A being Subset of X st A is dense holds
not A is empty
let A be Subset of X; :: thesis: ( A is dense implies not A is empty )
assume A is dense ; :: thesis: not A is empty
then A meets [#] X by TOPS145;
hence not A is empty ; :: thesis: verum