theorem Th19: :: OPPCAT_1:21

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