theorem :: PZFMISC1:36

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