for C being Category holds C is Subcategory of C