:: deftheorem Def6 defines full CAT_2:def 6 :
for D being Category
for C being Subcategory of D holds
( C is full iff for c1, c2 being Object of C
for d1, d2 being Object of D st c1 = d1 & c2 = d2 holds
Hom (c1,c2) = Hom (d1,d2) );