let k be odd Element of NAT ; :: thesis: ( (k -' 1) + 1 = k & ( for n being Element of NAT st k <= n holds
k -' 1 < n ) )
thus (k -' 1) + 1 = k by ABIAN:12, XREAL_1:235; :: thesis: for n being Element of NAT st k <= n holds
k -' 1 < n
let n be Element of NAT ; :: thesis: ( k <= n implies k -' 1 < n )
A1: k -' 1 < k by ABIAN:12, XREAL_1:237;
assume k <= n ; :: thesis: k -' 1 < n
hence k -' 1 < n by A1, XXREAL_0:2; :: thesis: verum