let X be non empty TopSpace; :: thesis: for A being Subset of X holds
( A is everywhere_dense iff ex C being Subset of X st
( C c= A & C is open & C is dense ) )
let A be Subset of X; :: thesis: ( A is everywhere_dense iff ex C being Subset of X st
( C c= A & C is open & C is dense ) )
thus ( A is everywhere_dense implies ex C being Subset of X st
( C c= A & C is open & C is dense ) ) :: thesis: ( ex C being Subset of X st
( C c= A & C is open & C is dense ) implies A is everywhere_dense )
proof
assume A1: A is everywhere_dense ; :: thesis: ex C being Subset of X st
( C c= A & C is open & C is dense )
take Int A ; :: thesis: ( Int A c= A & Int A is open & Int A is dense )
thus ( Int A c= A & Int A is open & Int A is dense ) by A1, TOPS_1:16; :: thesis: verum
end;
given C being Subset of X such that A2: ( C c= A & C is open & C is dense ) ; :: thesis: A is everywhere_dense
Int A is dense by A2, TOPS_1:24, TOPS_1:44;
hence A is everywhere_dense ; :: thesis: verum