let X be non empty TopSpace; :: thesis: for A, B being Subset of X st A is everywhere_dense & B is boundary holds
A \ B is dense
let A, B be Subset of X; :: thesis: ( A is everywhere_dense & B is boundary implies A \ B is dense )
assume A1: A is everywhere_dense ; :: thesis: ( not B is boundary or A \ B is dense )
A2: A \ B = A /\ (B `) by SUBSET_1:13;
assume B is boundary ; :: thesis: A \ B is dense
then B ` is dense by TOPS_1:def 4;
hence A \ B is dense by A1, A2, Th45; :: thesis: verum