theorem :: PZFMISC1:17

for I being set
for x, y being ManySortedSet of I st {x} (\/) {y} = {x} holds
x = y