let X, Y, Z be set ; :: thesis: (X \ Y) \ Z = X \ (Y \/ Z)
thus for x being set st x in (X \ Y) \ Z holds
x in X \ (Y \/ Z) :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: X \ (Y \/ Z) c= (X \ Y) \ Z

proof

let x be set ; :: thesis: ( x in (X \ Y) \ Z implies x in X \ (Y \/ Z) )
assume x in (X \ Y) \ Z ; :: thesis: x in X \ (Y \/ Z)
then ( x in X \ Y & not x in Z ) by XBOOLE_0:def 5;
then ( x in X & not x in Y & not x in Z ) by XBOOLE_0:def 5;
then ( x in X & not x in Y \/ Z ) by XBOOLE_0:def 3;
hence x in X \ (Y \/ Z) by XBOOLE_0:def 5; :: thesis: verum

end;

thus for x being set st x in X \ (Y \/ Z) holds
x in (X \ Y) \ Z :: according to TARSKI:def 3 :: thesis: verum

proof

let x be set ; :: thesis: ( x in X \ (Y \/ Z) implies x in (X \ Y) \ Z )
assume x in X \ (Y \/ Z) ; :: thesis: x in (X \ Y) \ Z
then ( x in X & not x in Y \/ Z ) by XBOOLE_0:def 5;
then ( x in X & not x in Y & not x in Z ) by XBOOLE_0:def 3;
then ( x in X \ Y & not x in Z ) by XBOOLE_0:def 5;
hence x in (X \ Y) \ Z by XBOOLE_0:def 5; :: thesis: verum

end;