let C be category; :: thesis: for o2, o1 being object of C st o2 is terminal & o1,o2 are_iso holds
o1 is terminal
let o2, o1 be object of C; :: thesis: ( o2 is terminal & o1,o2 are_iso implies o1 is terminal )
assume that
A1: o2 is terminal and
A2: o1,o2 are_iso ; :: thesis: o1 is terminal
for o3 being object of C ex M being Morphism of o3,o1 st
( M in <^o3,o1^> & ( for v being Morphism of o3,o1 st v in <^o3,o1^> holds
M = v ) )

proof

consider f being Morphism of o1,o2 such that
A3: f is iso by A2, ALTCAT_3:def 6;
A4: (f " ) * f = idm o1 by A3, ALTCAT_3:def 5;
let o3 be object of C; :: thesis: ex M being Morphism of o3,o1 st
( M in <^o3,o1^> & ( for v being Morphism of o3,o1 st v in <^o3,o1^> holds
M = v ) )
consider u being Morphism of o3,o2 such that
A5: u in <^o3,o2^> and
A6: for M1 being Morphism of o3,o2 st M1 in <^o3,o2^> holds
u = M1 by A1, ALTCAT_3:27;
take (f " ) * u ; :: thesis: ( (f " ) * u in <^o3,o1^> & ( for v being Morphism of o3,o1 st v in <^o3,o1^> holds
(f " ) * u = v ) )
A7: <^o2,o1^> <> {} by A2, ALTCAT_3:def 6;
then A8: <^o3,o1^> <> {} by A5, ALTCAT_1:def 4;
hence (f " ) * u in <^o3,o1^> ; :: thesis: for v being Morphism of o3,o1 st v in <^o3,o1^> holds
(f " ) * u = v
A9: <^o1,o2^> <> {} by A2, ALTCAT_3:def 6;
let v be Morphism of o3,o1; :: thesis: ( v in <^o3,o1^> implies (f " ) * u = v )
assume v in <^o3,o1^> ; :: thesis: (f " ) * u = v
f * v = u by A5, A6;
hence (f " ) * u = v by A4, A9, A7, A8, Th1; :: thesis: verum

end;

hence o1 is terminal by ALTCAT_3:27; :: thesis: verum