let C be Category; :: thesis: for c being Object of C holds
( c is initial iff c opp is terminal )
let c be Object of C; :: thesis: ( c is initial iff c opp is terminal )
thus ( c is initial implies c opp is terminal ) :: thesis: ( c opp is terminal implies c is initial )

proof

assume A1: c is initial ; :: thesis: c opp is terminal
let b be Object of (C opp); :: according to CAT_1:def 18 :: thesis: ( not Hom (b,(c opp)) = {} & ex b₁ being Morphism of b,c opp st
for b₂ being Morphism of b,c opp holds b₁ = b₂ )
consider f being Morphism of c, opp b such that
A2: for g being Morphism of c, opp b holds f = g by A1;
A3: (opp b) opp = b ;
A4: Hom (c,(opp b)) <> {} by A1;
reconsider f9 = f opp as Morphism of b,c opp ;
thus A5: Hom (b,(c opp)) <> {} by A3, Th4, A4; :: thesis: ex b₁ being Morphism of b,c opp st
for b₂ being Morphism of b,c opp holds b₁ = b₂
take f9 ; :: thesis: for b₁ being Morphism of b,c opp holds f9 = b₁
let g be Morphism of b,c opp ; :: thesis: f9 = g
opp (c opp) = c ;
then opp g is Morphism of c, opp b by A5, Th13;
hence g = f by A2
.= f9 by A4, Def6 ;
:: thesis: verum

end;

assume A6: c opp is terminal ; :: thesis: c is initial
let b be Object of C; :: according to CAT_1:def 19 :: thesis: ( not Hom (c,b) = {} & ex b₁ being Morphism of c,b st
for b₂ being Morphism of c,b holds b₁ = b₂ )
consider f being Morphism of b opp ,c opp such that
A7: for g being Morphism of b opp ,c opp holds f = g by A6;
A8: ( opp (c opp) = c & opp (b opp) = b ) ;
A9: Hom ((b opp),(c opp)) <> {} by A6;
reconsider f9 = opp f as Morphism of c,b ;
thus A10: Hom (c,b) <> {} by A8, Th5, A9; :: thesis: ex b₁ being Morphism of c,b st
for b₂ being Morphism of c,b holds b₁ = b₂
take f9 ; :: thesis: for b₁ being Morphism of c,b holds f9 = b₁
let g be Morphism of c,b; :: thesis: f9 = g
g opp = f by A7;
hence g = f by Def6, A10
.= f9 by A9, Def7 ;
:: thesis: verum