let A be set ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
thus ( x in union (bool A) implies x in A ) :: thesis:

proof

assume x in union (bool A) ; :: thesis:
then consider X being set such that
A1: x in X and
A2: X in bool A by TARSKI:def 4;
X c= A by A2, Def1;
hence x in A by A1; :: thesis:

end;

assume x in A ; :: thesis:
then {x} c= A by Lm1;
then A3: {x} in bool A by Def1;
x in {x} by TARSKI:def 1;
hence x in union (bool A) by A3, TARSKI:def 4; :: thesis:

end;

hence union (bool A) = A by TARSKI:2; :: thesis: