let C be Category; :: thesis: for a, b being Object of (C opp) holds Hom (a,b) = Hom ((opp b),(opp a))
let a, b be Object of (C opp); :: thesis: Hom (a,b) = Hom ((opp b),(opp a))
thus Hom (a,b) = Hom (((opp a) opp),((opp b) opp))
.= Hom ((opp b),(opp a)) by Th5 ; :: thesis: verum