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 )

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;

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