theorem :: ALTCAT_1:22

for C being non empty with_units AltCatStr holds
( C is pseudo-discrete iff for o being Object of C holds <^o,o^> = {(idm o)} )