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