let C be Category; :: thesis: for a being Object of C holds id a = id (a opp)
let a be Object of C; :: thesis: id a = id (a opp)
Hom (a,a) <> {} ;
hence id a = (id a) opp by Def6
.= id (a opp) by Th18 ;
:: thesis: verum