:: deftheorem Def18 defines pseudo-discrete NATTRA_1:def 19 :
for C being Category holds
( C is pseudo-discrete iff for a being Element of C holds Hom (a,a) is trivial );