theorem Th13: :: ALTCAT_1:19

for C being non empty with_units AltCatStr
for o being Object of C holds idm o in <^o,o^>