:: deftheorem defines pseudo-discrete ALTCAT_1:def 19 :
for C being AltCatStr holds
( C is pseudo-discrete iff for i being Object of C holds <^i,i^> is trivial );