theorem :: INDEX_1:39

for C being Category holds IdMap C = IdMap (C opp) by Lm2;