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