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