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