:: deftheorem defines are_isomorphic CAT_1:def 20 :
for C being Category
for a, b being Object of C holds
( a,b are_isomorphic iff ex f being Morphism of a,b st f is invertible );