let C be Category; for c being Object of C holds
( c is initial iff c opp is terminal )
let c be Object of C; ( c is initial iff c opp is terminal )
thus
( c is initial implies c opp is terminal )
( c opp is terminal implies c is initial )proof
assume A1:
c is
initial
;
c opp is terminal
let b be
Object of
(C opp);
CAT_1:def 18 ( not Hom (b,(c opp)) = {} & ex b1 being Morphism of b,c opp st
for b2 being Morphism of b,c opp holds b1 = b2 )
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;
ex b1 being Morphism of b,c opp st
for b2 being Morphism of b,c opp holds b1 = b2
take
f9
;
for b1 being Morphism of b,c opp holds f9 = b1
let g be
Morphism of
b,
c opp ;
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
;
verum
end;
assume A6:
c opp is terminal
; c is initial
let b be Object of C; CAT_1:def 19 ( not Hom (c,b) = {} & ex b1 being Morphism of c,b st
for b2 being Morphism of c,b holds b1 = b2 )
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; ex b1 being Morphism of c,b st
for b2 being Morphism of c,b holds b1 = b2
take
f9
; for b1 being Morphism of c,b holds f9 = b1
let g be Morphism of c,b; f9 = g
g opp = f
by A7;
hence g =
f
by Def6, A10
.=
f9
by A9, Def7
;
verum