let X be set ; :: thesis: union (BOOL X) = X
{} c= X by XBOOLE_1:2;
then ( BOOL X = (bool X) \ {{} } & {{} } c= bool X ) by ORDERS_1:def 2, ZFMISC_1:37;
then A1: (BOOL X) \/ {{} } c= bool X by 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;
then A2: bool X = (BOOL X) \/ {{} } by A1, XBOOLE_0:def 10;
X = union (bool X) by ZFMISC_1:99
.= (union (BOOL X)) \/ (union {{} }) by A2, ZFMISC_1:96
.= (union (BOOL X)) \/ {} by ZFMISC_1:31 ;
hence union (BOOL X) = X ; :: thesis: verum