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

proof

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

end;

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