c in COMPLEX by XCMPLX_0:def 2;
then c is Element of F_Complex by COMPLFLD:def 1;
hence In (c,F_Complex) = c by SUBSET_1:def 8; :: thesis: verum