:: deftheorem Def15 defines discrete CAT_6:def 15 :
for C being CategoryStr holds
( C is discrete iff for f being morphism of C holds f is identity );