let X be non empty TopSpace; :: thesis: for X1, X2 being SubSpace of X st X1 is nowhere_dense & X2 is SubSpace of X1 holds
X2 is nowhere_dense
let X1, X2 be SubSpace of X; :: thesis: ( X1 is nowhere_dense & X2 is SubSpace of X1 implies X2 is nowhere_dense )
assume A1: X1 is nowhere_dense ; :: thesis: ( not X2 is SubSpace of X1 or X2 is nowhere_dense )
assume X2 is SubSpace of X1 ; :: thesis: X2 is nowhere_dense
then the carrier of X2 c= the carrier of X1 by TSEP_1:4;
then for A being Subset of X st A = the carrier of X2 holds
A is nowhere_dense by A1, Th39;
hence X2 is nowhere_dense by Def4; :: thesis: verum