let C be Category; :: thesis: for a being Object of (C opp) holds opp (id a) = id (opp a)
let a be Object of (C opp); :: thesis: opp (id a) = id (opp a)
set b = opp a;
thus opp (id a) = id ((opp a) opp)
.= id (opp a) by Lm2 ; :: thesis: verum