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