let X be set ; :: thesis: union (BOOL X) = X
{} c= X ;
then ( BOOL X = (bool X) \ {{}} & {{}} c= bool X ) by ORDERS_1:def 3, ZFMISC_1:31;
then A1: (BOOL X) \/ {{}} c= bool X by XBOOLE_1:8;
(BOOL X) \/ {{}} = ((bool X) \ {{}}) \/ {{}} by ORDERS_1:def 3
.= (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:81
.= (union (BOOL X)) \/ (union {{}}) by A2, ZFMISC_1:78
.= (union (BOOL X)) \/ {} by ZFMISC_1:25 ;
hence union (BOOL X) = X ; :: thesis: verum