let n be Nat; :: thesis: 2 |^ n > n
2 |^ n >= n + 1 by Th104;
hence 2 |^ n > n by NAT_1:13; :: thesis: verum