let X be non empty TopSpace; :: thesis: for A being Subset of X holds
( A is nowhere_dense iff 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 ) )
let A be Subset of X; :: thesis: ( A is nowhere_dense iff 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 ) )
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: ( ( 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 ) ) implies A is nowhere_dense )

proof

assume A is nowhere_dense ; :: 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 & A misses H )
then A1: Cl A is boundary ;
let G be Subset of X; :: thesis: ( G <> {} & G is open implies ex H being Subset of X st
( H c= G & H <> {} & H is open & A misses H ) )
assume ( G <> {} & G is open ) ; :: thesis: ex H being Subset of X st
( H c= G & H <> {} & H is open & A misses H )
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: ( H c= G & H <> {} & H is open & A misses H )
thus ( H c= G & H <> {} & H is open & A misses H ) by A2, PRE_TOPC:18, XBOOLE_1:63; :: thesis: verum

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: A is nowhere_dense
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: ( G <> {} & G is open implies ex H being Subset of X st
( H c= G & H <> {} & H is open & Cl A misses H ) )
assume ( G <> {} & G is open ) ; :: thesis: ex H being Subset of X st
( H c= G & H <> {} & H is open & Cl A misses H )
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: ( H c= G & H <> {} & H is open & Cl A misses H )
thus ( H c= G & H <> {} & H is open & Cl A misses H ) by A4, TSEP_1:36; :: thesis: verum

end;

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