n >= 1 + 1 by NAT_2:29;
then n > 1 by NAT_1:13;
hence not Z/ n is degenerated by INT_3:11; :: thesis: verum