X in bool X by ZFMISC_1:def 1;
then X is Subset of X by Def2;
hence not for b₁ being Subset of X holds b₁ is empty ; :: thesis: verum