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

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