let C be Categorial Category; :: thesis: for a being Object of C holds a is Category
the carrier of C is categorial by Def6;
hence for a being Object of C holds a is Category by Def5; :: thesis: verum