let k, n be natural Number ; :: thesis: ( n < k implies (k -' (n + 1)) + 1 = k -' n )
assume A1: n < k ; :: thesis: (k -' (n + 1)) + 1 = k -' n
A2: k -' n = k - n by A1, XREAL_1:233;
n + 1 <= k by A1, NAT_1:13;
then k -' (n + 1) = k - (n + 1) by XREAL_1:233;
hence (k -' (n + 1)) + 1 = k -' n by A2; :: thesis: verum