theorem :: PZFMISC1:56

for I being set
for x, y, X being ManySortedSet of I st ( X = EmptyMS I or X = {x} or X = {y} or X = {x,y} ) holds
X (\) {x,y} = EmptyMS I