for A, B being Category st A,B are_equivalent holds
for F being Equivalence of A,B holds
( F is full & F is faithful & ( for b being Object of B ex a being Object of A st b,F . a are_isomorphic ) )