:: deftheorem Def4 defines Subcategory CAT_2:def 4 :
for C, b₂ being Category holds
( b₂ is Subcategory of C iff ( the carrier of b₂ c= the carrier of C & ( for a, b being Object of b₂
for a9, b9 being Object of C st a = a9 & b = b9 holds
Hom (a,b) c= Hom (a9,b9) ) & the Comp of b₂ c= the Comp of C & ( for a being Object of b₂
for a9 being Object of C st a = a9 holds
id a = id a9 ) ) );