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 x in X \/ Z ; :: thesis: x in Y \/ Z
then ( x in X or x in Z ) by XBOOLE_0:def 3;
then ( x in Y or x in Z ) by A1;
hence x in Y \/ Z by XBOOLE_0:def 3; :: thesis: verum