theorem :: OPPCAT_1:2

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