let c be Rational; :: thesis: c is g_rational
( Re c = c & Im c = 0 ) by COMPLEX1:def 1, COMPLEX1:def 2;
hence ( Re c in RAT & Im c in RAT ) by RAT_1:def 2; :: according to GAUSSINT:def 10 :: thesis: verum