:: deftheorem defines are_isomorphic ISOCAT_1:def 4 :
for A, B being Category holds
( A,B are_isomorphic iff ex F being Functor of A,B st F is isomorphic );