let C be Category; :: thesis: 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); :: thesis: 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; :: thesis: ( Hom (a,b) <> {} implies opp f is Morphism of opp b, opp a )
assume Hom (a,b) <> {} ; :: thesis: 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; :: thesis: verum