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