theorem :: PZFMISC1:11

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