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