theorem :: OPPCAT_1:72

for C being Category
for a being Object of (C opp) holds id a = id (opp a)