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