theorem :: ISOCAT_1:19

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