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