theorem Th15: :: SYSREL:15

for X, Y being set st X c= Y holds
id X c= id Y