theorem :: CAT_2:18

for C being Category
for E being Subcategory of C holds
( E is full iff incl E is full ) by Th13;