let X be non empty TopSpace; :: thesis: for X0 being SubSpace of X st X0 is nowhere_dense holds
for A being Subset of X st A c= the carrier of X0 holds
A is nowhere_dense
let X0 be SubSpace of X; :: thesis: ( X0 is nowhere_dense implies for A being Subset of X st A c= the carrier of X0 holds
A is nowhere_dense )
reconsider C = the carrier of X0 as Subset of X by TSEP_1:1;
assume X0 is nowhere_dense ; :: thesis: for A being Subset of X st A c= the carrier of X0 holds
A is nowhere_dense
then A1: C is nowhere_dense ;
let A be Subset of X; :: thesis: ( A c= the carrier of X0 implies A is nowhere_dense )
assume A c= the carrier of X0 ; :: thesis: A is nowhere_dense
hence A is nowhere_dense by A1, TOPS_3:26; :: thesis: verum