:: deftheorem Def2 defines union MBOOLEAN:def 2 :
for I being set
for A, b₃ being ManySortedSet of I holds
( b₃ = union A iff for i being object st i in I holds
b₃ . i = union (A . i) );