consider o being object such that
A: ( o in COMPLEX & not o in REAL ) by NUMBERS:1, XBOOLE_0:6;
reconsider c = o as Element of F_Complex by A, COMPLFLD:def 1;
not c is F_Real -membered by A, FIELD_7:def 5;
hence not for b₁ being Element of F_Complex holds b₁ is F_Real -membered ; :: thesis: verum