theorem :: CLASSES5:40

for U1, U2 being Universe
for x being Set of U1
for y being Set of U2 ex z being Set of sup (U1,U2) st
for a being object holds
( a in z iff ( a = x or a = y ) )