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

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