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