f
in
Hom
(
(
a
opp
)
,
(
b
opp
)
)
by
A1
,
CAT_1:def 5
;
then
f
in
Hom
(
b
,
a
)
by
Th4
;
hence
f
is
Morphism
of
b
,
a
by
CAT_1:def 5
;
:: thesis:
verum