let X be non empty TopSpace; :: thesis: for A being Subset of X st A is nowhere_dense holds
Cl A is nowhere_dense
let A be Subset of X; :: thesis: ( A is nowhere_dense implies Cl A is nowhere_dense )
assume A is nowhere_dense ; :: thesis: Cl A is nowhere_dense
then Cl A is boundary by TOPS_1:def 5;
hence Cl A is nowhere_dense ; :: thesis: verum