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

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