let X be non empty TopSpace; :: thesis: for X0 being non empty SubSpace of X
for A being Subset of X
for B being Subset of X0 st A c= B & B is nowhere_dense holds
A is nowhere_dense
let X0 be non empty SubSpace of X; :: thesis: for A being Subset of X
for B being Subset of X0 st A c= B & B is nowhere_dense holds
A is nowhere_dense
let A be Subset of X; :: thesis: for B being Subset of X0 st A c= B & B is nowhere_dense holds
A is nowhere_dense
let B be Subset of X0; :: thesis: ( A c= B & B is nowhere_dense implies A is nowhere_dense )
reconsider D = the carrier of X0 as Subset of X by TSEP_1:1;
reconsider G = (Int (Cl A)) /\ ([#] X0) as Subset of X0 ;
assume A1: A c= B ; :: thesis: ( not B is nowhere_dense or A is nowhere_dense )
then reconsider C = A as Subset of X0 by XBOOLE_1:1;
assume B is nowhere_dense ; :: thesis: A is nowhere_dense
then C is nowhere_dense by A1, Th26;
then A2: ( G is open & Int (Cl C) = {} ) by TOPS_2:24;
(Int (Cl A)) /\ ([#] X0) c= (Cl A) /\ ([#] X0) by TOPS_1:16, XBOOLE_1:26;
then A3: (Int (Cl A)) /\ ([#] X0) c= Cl C by PRE_TOPC:17;

now :: thesis: not Int (Cl A) <> {}

assume Int (Cl A) <> {} ; :: thesis: contradiction
then A meets Int (Cl A) by Th7;
then A4: A /\ (Int (Cl A)) <> {} ;
C c= D ;
then (Int (Cl A)) /\ D <> {} by A4, XBOOLE_1:3, XBOOLE_1:26;
hence contradiction by A3, A2, TOPS_1:24, XBOOLE_1:3; :: thesis: verum

end;

hence A is nowhere_dense ; :: thesis: verum