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