let X, Y be set ; :: thesis: ( union X c= Y implies X c= bool Y )
assume A1: ( union X c= Y & not X c= bool Y ) ; :: thesis: contradiction
then consider A being object such that
A2: ( A in X & not A in bool Y ) ;
reconsider AA = A as set by TARSKI:1;
AA c= Y by A2, A1, SETFAM_1:41;
hence contradiction by A2; :: thesis: verum