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 by Def4;
then [#] X c= Cl A by PRE_TOPC:19, TOPS_1:16;
then Cl A = [#] X by XBOOLE_0:def 10;
hence A is dense by TOPS_1:def 3; :: thesis: verum