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