ex x being non empty set st x in X by Def10;
hence not for b₁ being Element of X holds b₁ is empty ; :: thesis: verum