let X, Y be set ; :: thesis: ( X meets Y implies X /\ Y meets Y )
assume X meets Y ; :: thesis: X /\ Y meets Y
then consider x being object such that
A1: x in X and
A2: x in Y by XBOOLE_0:3;
x in X /\ Y by A1, A2, XBOOLE_0:def 4;
hence X /\ Y meets Y by A2, XBOOLE_0:3; :: thesis: verum