theorem :: PZFMISC1:55

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