theorem Th12: :: SYSREL:12
for X being set holds (id X) * (id X) = id X