let n be Element of NAT ; :: thesis: (2 * n) + 1 <= (2 * (n + 1)) + 1
(2 * (n + 1)) + 1 = ((2 * n) + 1) + 2 ;
hence (2 * n) + 1 <= (2 * (n + 1)) + 1 by NAT_1:11; :: thesis: verum