:: deftheorem defines disjoint-union CLASSES4:def 8 :
for UN being Universe
for I being Element of UN
for x being b₁ -valued ManySortedSet of I holds disjoint-union x = Union (disjoin x);