theorem Th1: :: NATTRA_1:5

for A being Category
for a being Object of A holds [[(id a),(id a)],(id a)] in the Comp of A