let X, Y, Z be set ; :: thesis: X /\ (Y \ Z) = (X /\ Y) \ Z

now :: thesis: for x being object holds

( x in X /\ (Y \ Z) iff x in (X /\ Y) \ Z )

hence
X /\ (Y \ Z) = (X /\ Y) \ Z
by TARSKI:2; :: thesis: verum( x in X /\ (Y \ Z) iff x in (X /\ Y) \ Z )

let x be object ; :: thesis: ( x in X /\ (Y \ Z) iff x in (X /\ Y) \ Z )

( x in X & x in Y & not x in Z iff ( x in X & x in Y & not x in Z ) ) ;

then ( x in X & x in Y \ Z iff ( x in X /\ Y & not x in Z ) ) by XBOOLE_0:def 4, XBOOLE_0:def 5;

hence ( x in X /\ (Y \ Z) iff x in (X /\ Y) \ Z ) by XBOOLE_0:def 4, XBOOLE_0:def 5; :: thesis: verum

end;( x in X & x in Y & not x in Z iff ( x in X & x in Y & not x in Z ) ) ;

then ( x in X & x in Y \ Z iff ( x in X /\ Y & not x in Z ) ) by XBOOLE_0:def 4, XBOOLE_0:def 5;

hence ( x in X /\ (Y \ Z) iff x in (X /\ Y) \ Z ) by XBOOLE_0:def 4, XBOOLE_0:def 5; :: thesis: verum