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

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

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

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

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

hence x in Z by A1; :: thesis: verum

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

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

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

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

hence x in Z by A1; :: thesis: verum