:: deftheorem defines are_iso ALTCAT_3:def 6 :
for C being category
for o1, o2 being Object of C holds
( o1,o2 are_iso iff ( <^o1,o2^> <> {} & <^o2,o1^> <> {} & ex A being Morphism of o1,o2 st A is iso ) );