theorem :: OPPCAT_1:4

for C being Category
for c being Object of (C opp) holds (opp c) opp = c ;