for n being odd Nat holds 1 <= n