:: deftheorem Def7 defines opp OPPCAT_1:def 7 :
for C being Category
for a, b being Object of C st Hom ((a opp),(b opp)) <> {} holds
for f being Morphism of a opp ,b opp holds opp f = f;