theorem :: PZFMISC1:20

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