:: deftheorem defines are_isomorphic CAT_7:def 10 :
for C being composable with_identities CategoryStr
for a, b being Object of C holds
( a,b are_isomorphic iff ex f being Morphism of a,b st f is isomorphism );