theorem :: CLASSES4:26

for UN being Universe
for I being Element of UN
for x being b₁ -valued ManySortedSet of I holds Union (coprod ) is Element of UN