let C be Category; for a, b being Object of (C opp)
for f being Morphism of a,b st Hom (a,b) <> {} holds
opp f is Morphism of opp b, opp a
let a, b be Object of (C opp); for f being Morphism of a,b st Hom (a,b) <> {} holds
opp f is Morphism of opp b, opp a
let f be Morphism of a,b; ( Hom (a,b) <> {} implies opp f is Morphism of opp b, opp a )
assume
Hom (a,b) <> {}
; opp f is Morphism of opp b, opp a
then
f in Hom (a,b)
by CAT_1:def 5;
then
opp f in Hom ((opp b),(opp a))
by Th5;
hence
opp f is Morphism of opp b, opp a
by CAT_1:def 5; verum