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 ;
hence contradiction by A1, TOPS_1:15; :: thesis: verum