theorem :: YELLOW20:40

for A, B being category
for F being contravariant Functor of A,B st A,B are_anti-isomorphic_under F holds
F is bijective