let k be odd Element of NAT ; :: thesis: ( 1 < k implies k - 2 is odd Element of NAT )
assume A1: 1 < k ; :: thesis: k - 2 is odd Element of NAT
consider i being Nat such that
A2: k = (2 * i) + 1 by ABIAN:9;
0 <> i by A1, A2;
then reconsider j = i - 1 as Nat by CHORD:1;
k - 2 = (2 * j) + 1 by A2;
hence k - 2 is odd Element of NAT ; :: thesis: verum