let n be Nat; :: thesis: n < (2 * n) + 1
assume (2 * n) + 1 <= n ; :: thesis: contradiction
then (2 * n) + 1 <= n + n by NAT_1:12;
hence contradiction by NAT_1:13; :: thesis: verum