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