theorem :: PZFMISC1:21

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