theorem :: ISOCAT_1:18

for A, B, C being Category holds [:[:A,B:],C:] ~= [:A,[:B,C:]:]