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