let X, Y, Z be set ; :: thesis: ( X c= Y /\ Z implies X c= Y )
Y /\ Z c= Y by Th17;
hence ( X c= Y /\ Z implies X c= Y ) by Th1; :: thesis: verum