let C be Categorial Category; :: thesis: for c being Object of C holds cat c = c
let c be Object of C; :: thesis: cat c = c
the carrier of C is categorial by Def6;
then c is Category ;
hence cat c = c by Def7; :: thesis: verum