let n be odd Nat; :: thesis: ( n - 1 is natural number & 1 <= n )
consider k being Element of NAT such that
A1: n = (2 * k) + 1 by ABIAN:9;
thus n - 1 is Nat by A1; :: thesis: 1 <= n
0 + 1 <= (2 * k) + 1 by XREAL_1:9;
hence 1 <= n by A1; :: thesis: verum