theorem :: GAUSSINT:7

for x being Element of Gauss_INT_Ring holds x is G_INTEG by Th2;