( REAL c= COMPLEX & 1 in REAL ) by NUMBERS:def 2, XBOOLE_1:7;
then 1 is complex number by Def2;
hence not for b₁ being complex number holds b₁ is zero ; :: thesis: verum