let X be set ; :: thesis: union (BOOL X) = X
A1: bool X = (BOOL X) \/ {{} }

proof

B1: BOOL X = (bool X) \ {{} } by ORDERS_1:def 2;
{} c= X by XBOOLE_1:2;
then {{} } c= bool X by ZFMISC_1:37;
then B2: (BOOL X) \/ {{} } c= bool X by B1, XBOOLE_1:8;
(BOOL X) \/ {{} } = ((bool X) \ {{} }) \/ {{} } by ORDERS_1:def 2
.= (bool X) \/ {{} } by XBOOLE_1:39 ;
then bool X c= (BOOL X) \/ {{} } by XBOOLE_1:7;
hence bool X = (BOOL X) \/ {{} } by B2, XBOOLE_0:def 10; :: thesis: verum

end;

X = union (bool X) by ZFMISC_1:99
.= (union (BOOL X)) \/ (union {{} }) by A1, ZFMISC_1:96
.= (union (BOOL X)) \/ {} by ZFMISC_1:31 ;
hence union (BOOL X) = X ; :: thesis: verum