for A, B, C being complex-membered set holds (A /// B) ** C = (A ** C) /// B by Th90;