let X be non empty TopSpace; :: thesis: for A being Subset of X holds
( A is nowhere_dense iff ex C being Subset of X st
( A c= C & C is closed & C is boundary ) )
let A be Subset of X; :: thesis: ( A is nowhere_dense iff ex C being Subset of X st
( A c= C & C is closed & C is boundary ) )
thus ( A is nowhere_dense implies ex C being Subset of X st
( A c= C & C is closed & C is boundary ) ) :: thesis: ( ex C being Subset of X st
( A c= C & C is closed & C is boundary ) implies A is nowhere_dense )
proof
assume A1: A is nowhere_dense ; :: thesis: ex C being Subset of X st
( A c= C & C is closed & C is boundary )
take Cl A ; :: thesis: ( A c= Cl A & Cl A is closed & Cl A is boundary )
thus ( A c= Cl A & Cl A is closed & Cl A is boundary ) by A1, PRE_TOPC:18; :: thesis: verum
end;
given C being Subset of X such that A2: ( A c= C & C is closed & C is boundary ) ; :: thesis: A is nowhere_dense
Cl A is boundary by A2, Th11, TOPS_1:5;
hence A is nowhere_dense ; :: thesis: verum