let U1, U2 be Universe; :: thesis: 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 ) )
let x be Set of U1; :: thesis: 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 ) )
let y be Set of U2; :: thesis: ex z being Set of sup (U1,U2) st
for a being object holds
( a in z iff ( a = x or a = y ) )
consider z being set such that
A1: for a being object holds
( a in z iff ( a = x or a = y ) ) by TARSKI_0:3;

per cases ( U1 in U2 or U2 in U1 or U1 = U2 ) by CLASSES2:52;

suppose A2: U1 in U2 ; :: thesis: ex z being Set of sup (U1,U2) st
for a being object holds
( a in z iff ( a = x or a = y ) )

then A3: sup (U1,U2) = U2 by Def13;
z in U2

proof

assume A4: not z in U2 ; :: thesis: contradiction
set X = {x,y};
( x is U1 -set & y is U2 -set ) by Def10;
then ( x in U2 & y in U2 ) by A2, CLASSES4:def 1;
then {x,y} in U2 by CLASSES2:58;
hence contradiction by A1, A4, TARSKI:def 2; :: thesis: verum

end;

then z is U2 -set ;
then reconsider z = z as Set of sup (U1,U2) by A3, Def10;
take z ; :: thesis: for a being object holds
( a in z iff ( a = x or a = y ) )
thus for a being object holds
( a in z iff ( a = x or a = y ) ) by A1; :: thesis: verum

end;

suppose A5: U2 in U1 ; :: thesis: ex z being Set of sup (U1,U2) st
for a being object holds
( a in z iff ( a = x or a = y ) )

then A6: sup (U1,U2) = U1 by Def13;
z in U1

proof

assume A7: not z in U1 ; :: thesis: contradiction
( x is U1 -set & y is U2 -set ) by Def10;
then ( x in U1 & y in U1 ) by A5, CLASSES4:def 1;
then {x,y} in U1 by CLASSES2:58;
hence contradiction by A1, A7, TARSKI:def 2; :: thesis: verum

end;

then z is U1 -set ;
then reconsider z = z as Set of sup (U1,U2) by A6, Def10;
take z ; :: thesis: for a being object holds
( a in z iff ( a = x or a = y ) )
thus for a being object holds
( a in z iff ( a = x or a = y ) ) by A1; :: thesis: verum

end;

suppose A8: U1 = U2 ; :: thesis: ex z being Set of sup (U1,U2) st
for a being object holds
( a in z iff ( a = x or a = y ) )

then A9: sup (U1,U2) = U1 by Def13;
z in U1

proof

assume A10: not z in U1 ; :: thesis: contradiction
( x is U1 -set & y is U2 -set ) by Def10;
then {x,y} in U1 by A8, CLASSES2:58;
hence contradiction by A1, A10, TARSKI:def 2; :: thesis: verum

end;

then z is U1 -set ;
then reconsider z = z as Set of sup (U1,U2) by A9, Def10;
take z ; :: thesis: for a being object holds
( a in z iff ( a = x or a = y ) )
thus for a being object holds
( a in z iff ( a = x or a = y ) ) by A1; :: thesis: verum

end;

end;