theorem :: PZFMISC1:43

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