let A, B, C be complex-membered set ; :: thesis: A /// (B /\ C) c= (A /// B) /\ (A /// C)
A /// (B /\ C) = A ** ((B "") /\ (C "")) by Th33;
hence A /// (B /\ C) c= (A /// B) /\ (A /// C) by Th93; :: thesis: verum