:: deftheorem defines disjoint-union CLASSES4:def 7 :
for UN being Universe
for x, y being Element of UN holds disjoint-union (x,y) = (x,y) --> (({} UN),{({} UN)});