let C be 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^> )
let o1, o2 be Object of (AllIso C); for m being Morphism of o1,o2 st <^o1,o2^> <> {} holds
( m is iso & m " in <^o2,o1^> )
let m be Morphism of o1,o2; ( <^o1,o2^> <> {} implies ( m is iso & m " in <^o2,o1^> ) )
assume A1:
<^o1,o2^> <> {}
; ( m is iso & m " in <^o2,o1^> )
reconsider p1 = o1, p2 = o2 as Object of C by Def5;
reconsider p = m as Morphism of p1,p2 by A1, ALTCAT_2:33;
p in the Arrows of (AllIso C) . (o1,o2)
by A1;
then A2:
( <^p1,p2^> <> {} & <^p2,p1^> <> {} )
by Def5;
A3:
p is iso
by A1, Def5;
then A4:
p " is iso
by A2, Th3;
then A5:
p " in the Arrows of (AllIso C) . (p2,p1)
by A2, Def5;
reconsider m1 = p " as Morphism of o2,o1 by A2, A4, Def5;
A6:
m is retraction
A7:
m is coretraction
p " in <^o2,o1^>
by A2, A4, Def5;
hence
m is iso
by A1, A6, A7, ALTCAT_3:6; m " in <^o2,o1^>
thus
m " in <^o2,o1^>
by A5; verum