:: deftheorem defines are_isomorphic CAT_6:def 28 :
for C, D being with_identities CategoryStr holds
( C,D are_isomorphic iff ex F being Functor of C,D ex G being Functor of D,C st
( F is covariant & G is covariant & G (*) F = id C & F (*) G = id D ) );