for A, B, A1, B1 being category
for F being FunctorStr over A,B st A1,B1 are_anti-isomorphic_under F holds
A1,B1 are_anti-isomorphic ;