:: deftheorem defines opp OPPCAT_1:def 2 :
for C being Category
for c being Object of C holds c opp = c;