theorem :: PZFMISC1:25

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