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

now :: thesis: for x being object st x in (X /\ Y) \/ (X /\ Z) holds
x in Y \/ Z

let x be object ; :: thesis: ( x in (X /\ Y) \/ (X /\ Z) implies x in Y \/ Z )
assume x in (X /\ Y) \/ (X /\ Z) ; :: thesis: x in Y \/ Z
then ( x in X /\ Y or x in X /\ Z ) by XBOOLE_0:def 3;
then ( ( x in X & x in Y ) or ( x in X & x in Z ) ) by XBOOLE_0:def 4;
hence x in Y \/ Z by XBOOLE_0:def 3; :: thesis: verum

end;

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