let X, Y, Z be set ; :: thesis: ( X misses Y implies X /\ (Y \/ Z) = X /\ Z )
assume X misses Y ; :: thesis: X /\ (Y \/ Z) = X /\ Z
then X /\ Y = {} ;
hence X /\ (Y \/ Z) = {} \/ (X /\ Z) by Th23
.= X /\ Z ;
:: thesis: verum