theorem Th69: :: OPPCAT_1:71

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