theorem :: CLASSES4:24

for UN being Universe
for x, y being Element of UN holds disjoint-union (x,y) is Subset of [:{x,y},{{},{{}}}:] by Lm1;