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

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