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 ; :: thesis: ( not Z c= V or X \/ Z c= Y \/ V )

assume 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 x in X \/ Z ; :: thesis: x in Y \/ V

then ( x in X or x in Z ) by XBOOLE_0:def 3;

then ( x in Y or x in V ) by A1, A2;

hence x in Y \/ V by XBOOLE_0:def 3; :: thesis: verum

assume A1: X c= Y ; :: thesis: ( not Z c= V or X \/ Z c= Y \/ V )

assume 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 x in X \/ Z ; :: thesis: x in Y \/ V

then ( x in X or x in Z ) by XBOOLE_0:def 3;

then ( x in Y or x in V ) by A1, A2;

hence x in Y \/ V by XBOOLE_0:def 3; :: thesis: verum