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

assume A1: X c= Y \/ 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 A2: x in X \ Y ; :: thesis: x in Z

then x in X by XBOOLE_0:def 5;

then A3: x in Y \/ Z by A1;

not x in Y by A2, XBOOLE_0:def 5;

hence x in Z by A3, XBOOLE_0:def 3; :: thesis: verum

assume A1: X c= Y \/ 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 A2: x in X \ Y ; :: thesis: x in Z

then x in X by XBOOLE_0:def 5;

then A3: x in Y \/ Z by A1;

not x in Y by A2, XBOOLE_0:def 5;

hence x in Z by A3, XBOOLE_0:def 3; :: thesis: verum