for n being odd Nat holds
( n - 1 is Nat & 1 <= n ) by Th1;