f in Hom (a,b) by Z, CAT_1:def 5;
then f in Hom ((b opp),(a opp)) by Th5;
hence f is Morphism of b opp ,a opp by CAT_1:def 5; :: thesis: verum