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

hence
(X /\ Y) \/ (X /\ Z) c= Y \/ Z
; :: thesis: verumx 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;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