let c be Complex; :: thesis: ( c is rational implies c is algebraic )
assume c is rational ; :: thesis: c is algebraic
then reconsider c = c as Element of F_Rat by RAT_1:def 2;
take In (c,F_Complex) ; :: according to ALGNUM_1:def 4 :: thesis: ( In (c,F_Complex) = c & In (c,F_Complex) is_integral_over F_Rat )
thus ( In (c,F_Complex) = c & In (c,F_Complex) is_integral_over F_Rat ) by Th3, Th27; :: thesis: verum