theorem :: INT_1:74

for n being non zero Nat holds
( n - 1 is Nat & 1 <= n )