theorem :: PZFMISC1:15

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