let X, Y, Z be set ; :: thesis: X /\ Y c= X \/ Z
( X /\ Y c= X & X c= X \/ Z ) by Th7, Th17;
hence X /\ Y c= X \/ Z ; :: thesis: verum