theorem Th25: :: EQREL_1:25

for X being set
for x being object st x in X holds
Class ((id X),x) = {x}