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)

proof

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 x in Y \/ Z by XBOOLE_0:def 4;
then A2: ( x in Y or x in Z ) by XBOOLE_0:def 3;
x in X by A1, XBOOLE_0:def 4;
then ( x in X /\ Y or x in X /\ Z ) by A2, XBOOLE_0:def 4;
hence x in (X /\ Y) \/ (X /\ Z) by XBOOLE_0:def 3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (X /\ Y) \/ (X /\ Z) or x in 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 A3: ( ( x in X & x in Y ) or ( x in X & x in Z ) ) by XBOOLE_0:def 4;
then x in Y \/ Z by XBOOLE_0:def 3;
hence x in X /\ (Y \/ Z) by A3, XBOOLE_0:def 4; :: thesis: verum