let c be Element of F_Complex ; :: thesis: c is complex
c in the carrier of F_Complex ;
then c in COMPLEX by Def1;
hence c is complex ; :: thesis: verum