let X be non empty TopSpace; :: thesis: for A, B being Subset of X st A is everywhere_dense & B is dense holds
A /\ B is dense
let A, B be Subset of X; :: thesis: ( A is everywhere_dense & B is dense implies A /\ B is dense )
assume A is everywhere_dense ; :: thesis: ( not B is dense or A /\ B is dense )
then A1: A ` is nowhere_dense by Th39;
assume B is dense ; :: thesis: A /\ B is dense
then A2: B ` is boundary by Th18;
A3: (A ` ) \/ (B ` ) = (A /\ B) ` by XBOOLE_1:54;
(A ` ) \/ (B ` ) is boundary by A1, A2, Th30;
hence A /\ B is dense by A3, Th18; :: thesis: verum