theorem Th39: :: GAUSSINT:39

for z being Element of Gauss_INT_Ring
for zz being G_INTEG st zz = z holds
( z is unital iff zz is g_int_unit )