theorem Th12: :: SYSREL:12

for X being set holds (id X) * (id X) = id X