theorem Th32: :: CLASSES4:32

for UN being Universe
for I, a, b, u, v being Element of UN
for x being b₁ -valued ManySortedSet of I st I = {a,b} & x . a = u & x . b = v holds
disjoint-union x = [:u,{a}:] \/ [:v,{b}:]