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

proof

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

end;

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