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