let X be non empty TopSpace; :: thesis: for A being Subset of X st A is everywhere_dense holds
A is dense
let A be Subset of X; :: thesis: ( A is everywhere_dense implies A is dense )
assume A is everywhere_dense ; :: thesis: A is dense
then Cl (Int A) = [#] X ;
then [#] X c= Cl A by PRE_TOPC:19, TOPS_1:16;
then Cl A = [#] X ;
hence A is dense ; :: thesis: verum