:: deftheorem defines discrete NATTRA_1:def 20 :
for C being Category holds
( C is discrete iff ( C is quasi-discrete & C is pseudo-discrete ) );