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

assume A1: X c= Y ; :: thesis: X /\ Z c= Y /\ Z

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

assume A2: x in X /\ Z ; :: thesis: x in Y /\ Z

then x in X by XBOOLE_0:def 4;

then A3: x in Y by A1;

x in Z by A2, XBOOLE_0:def 4;

hence x in Y /\ Z by A3, XBOOLE_0:def 4; :: thesis: verum

assume A1: X c= Y ; :: thesis: X /\ Z c= Y /\ Z

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

assume A2: x in X /\ Z ; :: thesis: x in Y /\ Z

then x in X by XBOOLE_0:def 4;

then A3: x in Y by A1;

x in Z by A2, XBOOLE_0:def 4;

hence x in Y /\ Z by A3, XBOOLE_0:def 4; :: thesis: verum