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