consider X being set such that
A1: for z being set holds
( z in X iff ( z in bool (bool (X1 \/ X2)) & S₁[z] ) ) from XBOOLE_0:sch 1();
take X ; :: thesis: for z being set holds
( z in X iff ex x, y being set st
( x in X1 & y in X2 & z = [x,y] ) )
let z be set ; :: thesis: ( z in X iff ex x, y being set st
( x in X1 & y in X2 & z = [x,y] ) )
thus ( z in X implies ex x, y being set st
( x in X1 & y in X2 & z = [x,y] ) ) by A1; :: thesis: ( ex x, y being set st
( x in X1 & y in X2 & z = [x,y] ) implies z in X )
given x, y being set such that A2: x in X1 and
A3: y in X2 and
A4: z = [x,y] ; :: thesis: z in X
( {x} c= X1 & X1 c= X1 \/ X2 ) by A2, Lm1, XBOOLE_1:7;
then {x} c= X1 \/ X2 by XBOOLE_1:1;
then A5: {x} in bool (X1 \/ X2) by Def1;
{x,y} c= X1 \/ X2

proof

let z be set ; :: 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 A2, A3, XBOOLE_0:def 3; :: thesis: verum

end;

then A6: {x,y} in bool (X1 \/ X2) by Def1;
{{x,y},{x}} c= bool (X1 \/ X2)

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in {{x,y},{x}} or z in bool (X1 \/ X2) )
assume z in {{x,y},{x}} ; :: thesis: z in bool (X1 \/ X2)
hence z in bool (X1 \/ X2) by A5, A6, TARSKI:def 2; :: thesis: verum

end;

then {{x,y},{x}} in bool (bool (X1 \/ X2)) by Def1;
hence z in X by A1, A2, A3, A4; :: thesis: verum