let C be Category; :: thesis: for a being Object of C holds id a is invertible
let a be Object of C; :: thesis: id a is invertible
( Hom (a,a) <> {} & (id a) * (id a) = id a ) ;
hence id a is invertible ; :: thesis: verum