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

( X \ (Y \/ Z) c= X \ Y & X \ (Y \/ Z) c= X \ Z ) by Th7, Th34;

hence X \ (Y \/ Z) c= (X \ Y) /\ (X \ Z) by Th19; :: according to XBOOLE_0:def 10 :: thesis: (X \ Y) /\ (X \ Z) c= X \ (Y \/ Z)

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

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

then A2: x in X \ Y by XBOOLE_0:def 4;

then A3: x in X by XBOOLE_0:def 5;

x in X \ Z by A1, XBOOLE_0:def 4;

then A4: not x in Z by XBOOLE_0:def 5;

not x in Y by A2, XBOOLE_0:def 5;

then not x in Y \/ Z by A4, XBOOLE_0:def 3;

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

( X \ (Y \/ Z) c= X \ Y & X \ (Y \/ Z) c= X \ Z ) by Th7, Th34;

hence X \ (Y \/ Z) c= (X \ Y) /\ (X \ Z) by Th19; :: according to XBOOLE_0:def 10 :: thesis: (X \ Y) /\ (X \ Z) c= X \ (Y \/ Z)

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

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

then A2: x in X \ Y by XBOOLE_0:def 4;

then A3: x in X by XBOOLE_0:def 5;

x in X \ Z by A1, XBOOLE_0:def 4;

then A4: not x in Z by XBOOLE_0:def 5;

not x in Y by A2, XBOOLE_0:def 5;

then not x in Y \/ Z by A4, XBOOLE_0:def 3;

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