theorem :: YELLOW18:18

for A, B, C, D being category st A,B are_opposite & C,D are_opposite & A,C are_isomorphic holds
B,D are_isomorphic