theorem Th18: :: OPPCAT_1:20

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