let X be non empty non almost_discrete TopSpace; :: thesis: for X0 being non empty SubSpace of X holds
( X0 is nowhere_dense iff ex X1 being non empty strict closed boundary SubSpace of X st X0 is SubSpace of X1 )
let X0 be non empty SubSpace of X; :: thesis: ( X0 is nowhere_dense iff ex X1 being non empty strict closed boundary SubSpace of X st X0 is SubSpace of X1 )
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
thus ( X0 is nowhere_dense implies ex X1 being non empty strict closed boundary SubSpace of X st X0 is SubSpace of X1 ) :: thesis: ( ex X1 being non empty strict closed boundary SubSpace of X st X0 is SubSpace of X1 implies X0 is nowhere_dense )

proof

assume X0 is nowhere_dense ; :: thesis: ex X1 being non empty strict closed boundary SubSpace of X st X0 is SubSpace of X1
then A is nowhere_dense ;
then consider C being Subset of X such that
A1: A c= C and
A2: ( C is closed & C is boundary ) by TOPS_3:27;
not C is empty by A1, XBOOLE_1:3;
then consider X1 being non empty strict closed boundary SubSpace of X such that
A3: C = the carrier of X1 by A2, Th67;
take X1 ; :: thesis: X0 is SubSpace of X1
thus X0 is SubSpace of X1 by A1, A3, TSEP_1:4; :: thesis: verum

end;

given X1 being non empty strict closed boundary SubSpace of X such that A4: X0 is SubSpace of X1 ; :: thesis: X0 is nowhere_dense
reconsider C = the carrier of X1 as Subset of X by TSEP_1:1;

now :: thesis: ex C being Subset of X st
( A c= C & C is boundary & C is closed )

take C = C; :: thesis: ( A c= C & C is boundary & C is closed )
thus ( A c= C & C is boundary & C is closed ) by A4, Def3, TSEP_1:4, TSEP_1:11; :: thesis: verum

end;

then for A being Subset of X st A = the carrier of X0 holds
A is nowhere_dense by TOPS_3:27;
hence X0 is nowhere_dense ; :: thesis: verum