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 :: thesis: not X /\ (Y /\ Z) = {}
assume A3: X /\ (Y /\ Z) = {} ; :: thesis: contradiction
X /\ Y = (X /\ Z) /\ Y by A2, Th28
.= {} by A3, Th16 ;
hence contradiction by A1; :: thesis: verum
end;
hence X meets Y /\ Z ; :: thesis: verum