:: deftheorem Def10 defines g_rational GAUSSINT:def 10 :
for z being Complex holds
( z is g_rational iff ( Re z in RAT & Im z in RAT ) );