let X be non empty TopSpace; :: thesis: for X0 being non empty SubSpace of X holds
( X0 is nowhere_dense iff ex X1 being non empty strict closed SubSpace of X st
( X1 is boundary & 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 SubSpace of X st
( X1 is boundary & 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 SubSpace of X st
( X1 is boundary & X0 is SubSpace of X1 ) ) :: thesis: ( ex X1 being non empty strict closed SubSpace of X st
( X1 is boundary & X0 is SubSpace of X1 ) implies X0 is nowhere_dense )

proof

assume X0 is nowhere_dense ; :: thesis: ex X1 being non empty strict closed SubSpace of X st
( X1 is boundary & 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 SubSpace of X such that
A3: ( X1 is boundary & C = the carrier of X1 ) by A2, Th41;
take X1 ; :: thesis: ( X1 is boundary & X0 is SubSpace of X1 )
thus ( X1 is boundary & X0 is SubSpace of X1 ) by A1, A3, TSEP_1:4; :: thesis: verum

end;

given X1 being non empty strict closed SubSpace of X such that A4: ( X1 is boundary & 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, 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