theorem :: PZFMISC1:9

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