theorem :: ISOCAT_1:17

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