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