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

thus for x being object st x in X \ (Y \ Z) holds

x in (X \ Y) \/ (X /\ Z) :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: (X \ Y) \/ (X /\ Z) c= X \ (Y \ Z)

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

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

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

then not x in Y \ Z by XBOOLE_0:def 5;

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

thus for x being object st x in X \ (Y \ Z) holds

x in (X \ Y) \/ (X /\ Z) :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: (X \ Y) \/ (X /\ Z) c= X \ (Y \ Z)

proof

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

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

then not x in Y \ Z by XBOOLE_0:def 5;

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

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

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

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

then not x in Y \ Z by XBOOLE_0:def 5;

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

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

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

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

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

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

then not x in Y \ Z by XBOOLE_0:def 5;

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