theorem :: PZFMISC1:30

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