theorem :: YELLOW18:19
for A, B, C, D being category st A,B are_opposite & C,D are_opposite & A,C are_anti-isomorphic holds
B,D are_anti-isomorphic