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