let n, i be Nat; :: thesis: ( 2 <= i implies i |^ n > n )
assume 2 <= i ; :: thesis: i |^ n > n
then i |^ n >= n + 1 by Th85;
hence i |^ n > n by NAT_1:13; :: thesis: verum