:: deftheorem Def20 defines IdCat NATTRA_1:def 21 :
for C being Category
for b₂ being strict Subcategory of C holds
( b₂ = IdCat C iff ( the carrier of b₂ = the carrier of C & the carrier' of b₂ = { (id a) where a is Object of C : verum } ) );