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