let X be non empty TopSpace; :: thesis: [#] X is everywhere_dense
Int ([#] X) = [#] X by TOPS_1:15;
then Cl (Int ([#] X)) = [#] X by TOPS_1:2;
hence [#] X is everywhere_dense ; :: thesis: verum