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