let X, Y, Z, V be set ; ( X c= Y & Z c= V implies X /\ Z c= Y /\ V )
assume that
A1:
X c= Y
and
A2:
Z c= V
; X /\ Z c= Y /\ V
let x be object ; TARSKI:def 3 ( not x in X /\ Z or x in Y /\ V )
assume A3:
x in X /\ Z
; 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; verum