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

now :: thesis: for x being object holds
( ( x in union (bool A) implies x in A ) & ( x in A implies x in union (bool A) ) )

let x be object ; :: 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; :: thesis: verum

end;

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

end;

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