let X, Y, Z be set ; :: thesis: ( X meets Y & X c= Z implies X meets Y /\ Z )
assume that
A1: X meets Y and
A2: X c= Z ; :: thesis: X meets Y /\ Z

now

assume A3: X /\ (Y /\ Z) = {} ; :: thesis: contradiction
X /\ Y = (X /\ Z) /\ Y by A2, Th28
.= {} by A3, Th16 ;
hence contradiction by A1, XBOOLE_0:def 7; :: thesis: verum

end;

hence X meets Y /\ Z by XBOOLE_0:def 7; :: thesis: verum