theorem :: MBOOLEAN:26
for I being set
for A, B being ManySortedSet of I st A c= B holds
union A c= union B