:: deftheorem defines g_prime GAUSSINT:def 22 :
for p being G_INTEG holds
( p is g_prime iff ( Norm p > 1 & ( for z being G_INTEG holds
( not z Divides p or z is g_int_unit or z is_associated_to p ) ) ) );