theorem Th1: :: FUNCT_3:1

for A, Y being set st A c= Y holds
id A = (id Y) | A