for A, B being Category st A,B are_equivalent holds
for F being Equivalence of A,B ex G being Equivalence of B,A st
( G * F ~= id A & F * G ~= id B )