let c be Element of F_Complex; :: thesis: ( c is algebraic iff ex f being INT -valued non-zero Polynomial of F_Complex st c is_a_root_of f )

hereby :: thesis: ( ex f being INT -valued non-zero Polynomial of F_Complex st c is_a_root_of f implies c is algebraic )

assume c is algebraic ; :: thesis: ex f being INT -valued non-zero Polynomial of F_Complex st c is_a_root_of f
then ex f being RAT -valued monic Polynomial of F_Complex st c is_a_root_of f by Th25;
hence ex f being INT -valued non-zero Polynomial of F_Complex st c is_a_root_of f by Th24; :: thesis: verum

end;

assume ex f being INT -valued non-zero Polynomial of F_Complex st c is_a_root_of f ; :: thesis: c is algebraic
then ex f being RAT -valued monic Polynomial of F_Complex st c is_a_root_of f by Th24;
hence c is algebraic by Th25; :: thesis: verum