theorem :: MBOOLEAN:28

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