( X is empty or not X is empty ) ;
hence for b₁ being Element of X holds b₁ is natural-valued by Def7, SUBSET_1:def 1; :: thesis: verum