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