theorem :: YELLOW18:16

for A, B being category st A,B are_opposite holds
A,B are_anti-isomorphic