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