theorem :: OPPCAT_1:3

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