let X be non empty TopSpace; :: thesis: for X0 being SubSpace of X
for A being Subset of X st A = the carrier of X0 holds
( X0 is nowhere_dense iff A is nowhere_dense )
let X0 be SubSpace of X; :: thesis: for A being Subset of X st A = the carrier of X0 holds
( X0 is nowhere_dense iff A is nowhere_dense )
let A be Subset of X; :: thesis: ( A = the carrier of X0 implies ( X0 is nowhere_dense iff A is nowhere_dense ) )
assume A1: A = the carrier of X0 ; :: thesis: ( X0 is nowhere_dense iff A is nowhere_dense )
hence ( X0 is nowhere_dense implies A is nowhere_dense ) by Def4; :: thesis: ( A is nowhere_dense implies X0 is nowhere_dense )
assume A is nowhere_dense ; :: thesis: X0 is nowhere_dense
then for B being Subset of X st B = the carrier of X0 holds
B is nowhere_dense by A1;
hence X0 is nowhere_dense by Def4; :: thesis: verum