theorem :: PZFMISC1:14

for I being set
for x, A, B being ManySortedSet of I st {x} = {A,B} holds
( x = A & x = B )