theorem Th2: :: YELLOW21:2

for C being set-id-inheriting carrier-underlaid category
for a being Object of C holds idm a = id (a as_1-sorted)