theorem :: PZFMISC1:32

for I being set
for A, B being ManySortedSet of I holds union {A,B} = A (\/) B