theorem :: PZFMISC1:44

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