let X, Y, Z be set ; :: thesis: ( X c= Y & X misses Z implies X c= Y \ Z )
assume A1: ( X c= Y & X /\ Z = {} ) ; :: according to XBOOLE_0:def 7 :: 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 Y & not x in Z ) by A1, XBOOLE_0:def 4;
hence x in Y \ Z by XBOOLE_0:def 5; :: thesis: verum