theorem :: GAUSSINT:8

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