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