theorem :: PZFMISC1:10

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