theorem Th18: :: FUNCT_1:18

for X being set
for x being object st x in X holds
(id X) . x = x by Th17;