let X, Y, Z, V be set ; :: thesis: ( X c= Y & Z c= V implies X /\ Z c= Y /\ V )

assume that

A1: X c= Y and

A2: Z c= V ; :: thesis: X /\ Z c= Y /\ V

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X /\ Z or x in Y /\ V )

assume A3: x in X /\ Z ; :: thesis: x in Y /\ V

then x in Z by XBOOLE_0:def 4;

then A4: x in V by A2;

x in X by A3, XBOOLE_0:def 4;

then x in Y by A1;

hence x in Y /\ V by A4, XBOOLE_0:def 4; :: thesis: verum

assume that

A1: X c= Y and

A2: Z c= V ; :: thesis: X /\ Z c= Y /\ V

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X /\ Z or x in Y /\ V )

assume A3: x in X /\ Z ; :: thesis: x in Y /\ V

then x in Z by XBOOLE_0:def 4;

then A4: x in V by A2;

x in X by A3, XBOOLE_0:def 4;

then x in Y by A1;

hence x in Y /\ V by A4, XBOOLE_0:def 4; :: thesis: verum