theorem Th96: :: FUNCT_4:96

for x being object holds x .--> x = id {x}