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

thus (X \/ Y) \ Z c= (X \ Z) \/ (Y \ Z) :: according to XBOOLE_0:def 10 :: thesis: (X \ Z) \/ (Y \ Z) c= (X \/ Y) \ Z

assume x in (X \ Z) \/ (Y \ Z) ; :: thesis: x in (X \/ Y) \ Z

then ( x in X \ Z or x in Y \ Z ) by XBOOLE_0:def 3;

then A2: ( ( x in X & not x in Z ) or ( x in Y & not x in Z ) ) by XBOOLE_0:def 5;

then x in X \/ Y by XBOOLE_0:def 3;

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

thus (X \/ Y) \ Z c= (X \ Z) \/ (Y \ Z) :: according to XBOOLE_0:def 10 :: thesis: (X \ Z) \/ (Y \ Z) c= (X \/ Y) \ Z

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (X \ Z) \/ (Y \ Z) or x in (X \/ Y) \ Z )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (X \/ Y) \ Z or x in (X \ Z) \/ (Y \ Z) )

assume A1: x in (X \/ Y) \ Z ; :: thesis: x in (X \ Z) \/ (Y \ Z)

then x in X \/ Y by XBOOLE_0:def 5;

then ( ( x in X & not x in Z ) or ( x in Y & not x in Z ) ) by A1, XBOOLE_0:def 3, XBOOLE_0:def 5;

then ( x in X \ Z or x in Y \ Z ) by XBOOLE_0:def 5;

hence x in (X \ Z) \/ (Y \ Z) by XBOOLE_0:def 3; :: thesis: verum

end;assume A1: x in (X \/ Y) \ Z ; :: thesis: x in (X \ Z) \/ (Y \ Z)

then x in X \/ Y by XBOOLE_0:def 5;

then ( ( x in X & not x in Z ) or ( x in Y & not x in Z ) ) by A1, XBOOLE_0:def 3, XBOOLE_0:def 5;

then ( x in X \ Z or x in Y \ Z ) by XBOOLE_0:def 5;

hence x in (X \ Z) \/ (Y \ Z) by XBOOLE_0:def 3; :: thesis: verum

assume x in (X \ Z) \/ (Y \ Z) ; :: thesis: x in (X \/ Y) \ Z

then ( x in X \ Z or x in Y \ Z ) by XBOOLE_0:def 3;

then A2: ( ( x in X & not x in Z ) or ( x in Y & not x in Z ) ) by XBOOLE_0:def 5;

then x in X \/ Y by XBOOLE_0:def 3;

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