for c being Element of F_Complex holds
( c is algebraic_integer iff ex f being INT -valued monic Polynomial of F_Complex st c is_a_root_of f )