let X, Y, Z, V be set ; :: thesis: ( X c= Y & Z c= V implies X /\ Z c= Y /\ V )
assume A1: ( X c= Y & Z c= V ) ; :: thesis: X /\ Z c= Y /\ V
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X /\ Z or x in Y /\ V )
assume x in X /\ Z ; :: thesis: x in Y /\ V
then ( x in X & x in Z ) by XBOOLE_0:def 4;
then ( x in Y & x in V ) by A1, TARSKI:def 3;
hence x in Y /\ V by XBOOLE_0:def 4; :: thesis: verum