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