theorem :: PZFMISC1:24

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