let c be Integer; :: thesis: c is g_integer
( Re c = c & Im c = 0 ) by COMPLEX1:def 1, COMPLEX1:def 2;
hence ( Re c in INT & Im c in INT ) by INT_1:def 2; :: according to GAUSSINT:def 1 :: thesis: verum