let A, B, C be complex-membered set ; :: thesis: A /// (B \/ C) = (A /// B) \/ (A /// C)
thus A /// (B \/ C) = A ** ((B "") \/ (C "")) by Th32
.= (A /// B) \/ (A /// C) by Th92 ; :: thesis: verum