theorem Th52: :: ENUMSET1:52
for x1, x2 being object holds {x1,x1,x1,x1,x1,x1,x2} = {x1,x2}