let C be Category; :: thesis: for a, b being Object of C holds Hom (a,b) = Hom ((b opp),(a opp))
let a, b be Object of C; :: thesis: Hom (a,b) = Hom ((b opp),(a opp))
thus Hom (a,b) c= Hom ((b opp),(a opp)) :: according to XBOOLE_0:def 10 :: thesis: Hom ((b opp),(a opp)) c= Hom (a,b)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Hom (a,b) or x in Hom ((b opp),(a opp)) )
assume A1: x in Hom (a,b) ; :: thesis: x in Hom ((b opp),(a opp))
then reconsider f = x as Morphism of C ;
reconsider g = f as Morphism of (C opp) ;
( dom f = a & cod f = b ) by A1, CAT_1:1;
then ( dom g = b opp & cod g = a opp ) ;
hence x in Hom ((b opp),(a opp)) ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Hom ((b opp),(a opp)) or x in Hom (a,b) )
assume A2: x in Hom ((b opp),(a opp)) ; :: thesis: x in Hom (a,b)
then reconsider f = x as Morphism of (C opp) ;
reconsider g = f as Morphism of C ;
( dom f = b opp & cod f = a opp ) by A2, CAT_1:1;
then ( dom g = a & cod g = b ) ;
hence x in Hom (a,b) ; :: thesis: verum