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

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
A3: u in <^o3,o2^> and
A4: for M1 being Morphism of o3,o2 st M1 in <^o3,o2^> holds
u = M1 by A1, ALTCAT_3:27;
consider f being Morphism of o1,o2 such that
A5: f is iso by A2, ALTCAT_3:def 6;
A6: (f " ) * f = idm o1 by A5, ALTCAT_3:def 5;
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: ( <^o1,o2^> <> {} & <^o2,o1^> <> {} ) by A2, ALTCAT_3:def 6;
then A8: <^o3,o1^> <> {} by A3, 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
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 A3, A4;
hence (f " ) * u = v by A6, A7, A8, Th1; :: thesis: verum

end;

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