not bool X c= X by CARD_1:25;
hence for b₁ being set st b₁ = (bool X) \ X holds
not b₁ is empty by XBOOLE_1:37; :: thesis: verum