theorem :: CLASSES4:34

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} & u <> v holds
disjoint-union x = disjoint-union (u,v)