theorem :: MBOOLEAN:27

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