let c be Complex; :: thesis: ( c is integer implies c is algebraic_integer )
assume c is integer ; :: thesis: c is algebraic_integer
then reconsider c = c as Element of INT.Ring by INT_1:def 2;
take In (c,F_Complex) ; :: according to ALGNUM_1:def 6 :: thesis: ( In (c,F_Complex) = c & In (c,F_Complex) is_integral_over INT.Ring )
thus ( In (c,F_Complex) = c & In (c,F_Complex) is_integral_over INT.Ring ) by Th4, Th27; :: thesis: verum