for C being Category
for E being Subcategory of C holds incl E is faithful