let X be non empty TopSpace; :: thesis: for A, B being Subset of X st B is nowhere_dense & A c= B holds
A is nowhere_dense
let A, B be Subset of X; :: thesis: ( B is nowhere_dense & A c= B implies A is nowhere_dense )
assume B is nowhere_dense ; :: thesis: ( not A c= B or A is nowhere_dense )
then A1: Cl B is boundary ;
assume A c= B ; :: thesis: A is nowhere_dense
then Cl A is boundary by A1, Th11, PRE_TOPC:19;
hence A is nowhere_dense ; :: thesis: verum