A1: X1 c= X1 \/ X2 by XBOOLE_1:7;
consider X being set such that
A2: for z being object holds
( z in X iff ( z in bool (bool (X1 \/ X2)) & S1[z] ) ) from XBOOLE_0:sch 1();
 take X ; :: thesis: for z being object holds
( z in X iff ex x, y being object st
( x in X1 & y in X2 & z = [x,y] ) )
let z be object ; :: thesis: ( z in X iff ex x, y being object st
( x in X1 & y in X2 & z = [x,y] ) )
thus ( z in X implies ex x, y being object st
( x in X1 & y in X2 & z = [x,y] ) ) by A2; :: thesis: ( ex x, y being object st
( x in X1 & y in X2 & z = [x,y] ) implies z in X )
given x, y being object such that A3: x in X1 and
A4: y in X2 and
A5: z = [x,y] ; :: thesis: z in X
{x,y} c= X1 \/ X2
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in {x,y} or z in X1 \/ X2 )
assume z in {x,y} ; :: thesis: z in X1 \/ X2
then ( z = x or z = y ) by TARSKI:def 2;
hence z in X1 \/ X2 by A3, A4, XBOOLE_0:def 3; :: thesis: verum
end;
then A6: {x,y} in bool (X1 \/ X2) by Def1;
{x} c= X1 \/ X2 by A1, A3, Lm1;
then A7: {x} in bool (X1 \/ X2) by Def1;
{{x,y},{x}} c= bool (X1 \/ X2) by A7, A6, TARSKI:def 2;
then {{x,y},{x}} in bool (bool (X1 \/ X2)) by Def1;
hence z in X by A2, A3, A4, A5; :: thesis: verum