let X be non empty TopSpace; :: thesis: for A being Subset of X st A is nowhere_dense holds
not A is dense
let A be Subset of X; :: thesis: ( A is nowhere_dense implies not A is dense )
assume A1: Int (Cl A) = {} ; :: according to TOPS_3:def 3 :: thesis: not A is dense
assume A is dense ; :: thesis: contradiction
then Cl A = [#] X by TOPS_1:def 3;
hence contradiction by A1, TOPS_1:43; :: thesis: verum