let X, Y be set ; :: thesis: UNION ((bool X),(bool Y)) = bool (X \/ Y)
thus UNION ((bool X),(bool Y)) c= bool (X \/ Y) :: according to XBOOLE_0:def 10 :: thesis: bool (X \/ Y) c= UNION ((bool X),(bool Y))

proof

let xy be object ; :: according to TARSKI:def 3 :: thesis: ( not xy in UNION ((bool X),(bool Y)) or xy in bool (X \/ Y) )
assume xy in UNION ((bool X),(bool Y)) ; :: thesis: xy in bool (X \/ Y)
then consider x, y being set such that
A1: ( x in bool X & y in bool Y & xy = x \/ y ) by SETFAM_1:def 4;
x \/ y c= X \/ Y by A1, XBOOLE_1:13;
hence xy in bool (X \/ Y) by A1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in bool (X \/ Y) or x in UNION ((bool X),(bool Y)) )
reconsider A = x as set by TARSKI:1;
assume x in bool (X \/ Y) ; :: thesis: x in UNION ((bool X),(bool Y))
then A2: A \ X c= Y by XBOOLE_1:43;
A /\ X c= X by XBOOLE_1:17;
then (A /\ X) \/ (A \ X) in UNION ((bool X),(bool Y)) by A2, SETFAM_1:def 4;
hence x in UNION ((bool X),(bool Y)) ; :: thesis: verum