theorem :: PZFMISC1:33

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