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

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

hence (X \ Y) \/ (X \ Z) c= X \ (Y /\ Z) by Th8; :: thesis: verum

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

proof

( X \ Y c= X \ (Y /\ Z) & X \ Z c= X \ (Y /\ Z) )
by Th17, Th34;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X \ (Y /\ Z) or 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 A2: ( not x in Y or not x in Z ) by XBOOLE_0:def 4;

x in X by A1, XBOOLE_0:def 5;

then ( x in X \ Y or x in X \ Z ) by A2, 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 A2: ( not x in Y or not x in Z ) by XBOOLE_0:def 4;

x in X by A1, XBOOLE_0:def 5;

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

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

hence (X \ Y) \/ (X \ Z) c= X \ (Y /\ Z) by Th8; :: thesis: verum