let X be non empty TopSpace; :: thesis: for A being Subset of X holds
( A is everywhere_dense iff Int A is dense )
let A be Subset of X; :: thesis: ( A is everywhere_dense iff Int A is dense )
thus ( A is everywhere_dense implies Int A is dense ) by Th32, Th33; :: thesis: ( Int A is dense implies A is everywhere_dense )
assume Int A is dense ; :: thesis: A is everywhere_dense
then Cl (Int A) = [#] X by TOPS_1:def 3;
hence A is everywhere_dense by Def4; :: thesis: verum