:: deftheorem Def16 defines DiscreteCat CAT_6:def 16 :
for X being set
for b₂ being strict discrete category holds
( b₂ = DiscreteCat X iff the carrier of b₂ = X );