theorem :: MBOOLEAN:30

for I being set
for A being ManySortedSet of I holds A c= bool (union A)