let X be non empty TopSpace; :: thesis: for A, B being Subset of X st ( ( A is everywhere_dense & B is dense ) or ( A is dense & B is everywhere_dense ) ) holds
A meets B
let A, B be Subset of X; :: thesis: ( ( ( A is everywhere_dense & B is dense ) or ( A is dense & B is everywhere_dense ) ) implies A meets B )
assume ( ( A is everywhere_dense & B is dense ) or ( A is dense & B is everywhere_dense ) ) ; :: thesis: A meets B
then A /\ B <> {} by TOPS_3:17, TOPS_3:45;
hence A meets B by XBOOLE_0:def 7; :: thesis: verum