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 ; :: thesis: verum