theorem :: CLASSES4:25

for UN being Universe
for u being Element of UN holds disjoint-union (u,u) = {[u,{{}}]}