:: deftheorem Def20 defines g_int_unit GAUSSINT:def 20 :
for z being G_INTEG holds
( z is g_int_unit iff Norm z = 1 );