theorem Th1: :: ALTCAT_3:1

for C being non empty with_units AltCatStr
for o being Object of C holds
( idm o is retraction & idm o is coretraction )