theorem :: CAT_2:16

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