:: deftheorem Def11 defines Equivalence ISOCAT_1:def 11 :
for A, B being Category st A,B are_equivalent holds
for b₃ being Functor of A,B holds
( b₃ is Equivalence of A,B iff ex G being Functor of B,A st
( G * b₃ ~= id A & b₃ * G ~= id B ) );