:: deftheorem defines opp OPPCAT_1:def 4 :
for C being Category
for f being Morphism of C holds f opp = f;