let c be Complex; :: thesis: ( c is algebraic_integer implies c is algebraic )
assume A1: c is algebraic_integer ; :: thesis: c is algebraic
c in COMPLEX by XCMPLX_0:def 2;
then reconsider c = c as Element of F_Complex by COMPLFLD:def 1;
ex f being INT -valued monic Polynomial of F_Complex st c is_a_root_of f by A1, Th27;
hence c is algebraic by Th26; :: thesis: verum