theorem Th56: :: CLASSES5:54

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