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

assume A1: for x being object st x in X \ Y holds

x in Z ; :: according to TARSKI:def 3 :: thesis: X c= Y \/ Z

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

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

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

then ( x in Z or x in Y ) by A1;

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

assume A1: for x being object st x in X \ Y holds

x in Z ; :: according to TARSKI:def 3 :: thesis: X c= Y \/ Z

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

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

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

then ( x in Z or x in Y ) by A1;

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