let A be set ; :: thesis: union (bool A) = A

now

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

proof

assume x in union (bool A) ; :: thesis: x in A
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, TARSKI:def 3; :: thesis: verum

end;

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

end;

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