theorem :: PZFMISC1:52

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