theorem :: PZFMISC1:45

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