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 & Cl A is closed ) by TOPS_1:def 5;
hence Cl A is nowhere_dense ; :: thesis: verum