let X be non empty TopSpace; :: thesis: for B, A being Subset of X st B is nowhere_dense & A c= B holds
A is nowhere_dense
let B, A 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 by TOPS_1:def 5;
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 by TOPS_1:def 5; :: thesis: verum