for n being Element of NAT holds ((n ^2) - n) + 1 > 0 by Lm21;