theorem Th52: :: ALTCAT_4:52

for C being category
for o1, o2 being Object of (AllIso C)
for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
( m is iso & m " in <^o2,o1^> )