theorem :: PZFMISC1:13

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