let X, Y be set ; :: thesis: [:X,Y:] c= bool (bool (X \/ Y))
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in [:X,Y:] or z in bool (bool (X \/ Y)) )
assume z in [:X,Y:] ; :: thesis: z in bool (bool (X \/ Y))
then consider x, y being set such that
A1: x in X and
A2: y in Y and
A3: z = [x,y] by Def2;
z c= bool (X \/ Y)

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in z or u in bool (X \/ Y) )
assume A4: u in z ; :: thesis: u in bool (X \/ Y)
( X c= X \/ Y & {x} c= X & x in X \/ Y & y in X \/ Y ) by A1, A2, Lm1, XBOOLE_0:def 3, XBOOLE_1:7;
then ( {x} c= X \/ Y & {x,y} c= X \/ Y & ( u = {x,y} or u = {x} ) ) by A3, A4, Th38, TARSKI:def 2, XBOOLE_1:1;
hence u in bool (X \/ Y) by Def1; :: thesis: verum

end;

hence z in bool (bool (X \/ Y)) by Def1; :: thesis: verum