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