let X be non empty TopSpace; :: thesis:
let A be Subset of X; :: thesis:
thus ( A is nowhere_dense implies for G being Subset of X st G <> {} & G is open holds
ex H being Subset of X st
( H c= G & H <> {} & H is open & A misses H ) ) :: thesis:

proof

assume A is nowhere_dense ; :: thesis:
then A1: Cl A is boundary ;
let G be Subset of X; :: thesis:
assume ( G <> {} & G is open ) ; :: thesis:
then consider H being Subset of X such that
A2: ( H c= G & H <> {} & H is open & Cl A misses H ) by A1, TOPS_1:51;
take H ; :: thesis:
thus ( H c= G & H <> {} & H is open & A misses H ) by A2, PRE_TOPC:18, XBOOLE_1:63; :: thesis:

end;

assume A3: for G being Subset of X st G <> {} & G is open holds
ex H being Subset of X st
( H c= G & H <> {} & H is open & A misses H ) ; :: thesis:
for G being Subset of X st G <> {} & G is open holds
ex H being Subset of X st
( H c= G & H <> {} & H is open & Cl A misses H )

proof

let G be Subset of X; :: thesis:
assume ( G <> {} & G is open ) ; :: thesis:
then consider H being Subset of X such that
A4: ( H c= G & H <> {} & H is open & A misses H ) by A3;
take H ; :: thesis:
thus ( H c= G & H <> {} & H is open & Cl A misses H ) by A4, TSEP_1:36; :: thesis:

end;

then Cl A is boundary by TOPS_1:51;
hence A is nowhere_dense ; :: thesis: