theorem :: MBOOLEAN:31

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