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

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

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

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

then ( x in X & x in Y ) by A1;

hence x in X /\ Y by XBOOLE_0:def 4; :: thesis: verum

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

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

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

then ( x in X & x in Y ) by A1;

hence x in X /\ Y by XBOOLE_0:def 4; :: thesis: verum