let X, Y, Z be set ; :: thesis: ( X c= Z & Y = Z \ X implies X c= Z \ Y )
assume that
A1: X c= Z and
A2: Y = Z \ X ; :: thesis: X c= Z \ Y
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Z \ Y )
assume A3: x in X ; :: thesis: x in Z \ Y
then not x in Y by A2, XBOOLE_0:def 5;
hence x in Z \ Y by A1, A3, XBOOLE_0:def 5; :: thesis: verum