theorem :: CLASSES4:27

for UN being Universe
for I being Element of UN
for x being b₁ -valued ManySortedSet of I holds disjoint-union x is Subset of [:(union (rng x)),I:]