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