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