theorem :: PZFMISC1:31

for I being set
for x, y being ManySortedSet of I holds union {{x},{y}} = {x,y}