theorem Th33: :: CLASSES4:33

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