:: deftheorem defines are_anti-isomorphic FUNCTOR0:def 40 :
for A, B being non empty transitive with_units AltCatStr holds
( A,B are_anti-isomorphic iff ex F being Functor of A,B st
( F is bijective & F is contravariant ) );