theorem :: MBOOLEAN:25

for I being set
for A, X being ManySortedSet of I st X in A holds
X c= union A