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