let n, k be Nat; :: thesis: ( n > 1 implies n |^|^ k > k )
assume A0: n > 1 ; :: thesis: n |^|^ k > k
defpred S₁[ Nat] means n |^|^ $1 > $1;
A1: S₁[ 0 ] by Th0;

A2: now

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
succ k = k + 1 by NAT_1:39;
then n |^|^ (k + 1) = exp n,(n |^|^ k) by Th1
.= n |^ (n |^|^ k) by LemExp ;
then A4: n |^|^ (k + 1) > n |^ k by A0, A3, PEPIN:71;
n |^ k > k by A0, NAT_4:3;
then n |^ k >= k + 1 by NAT_1:13;
hence S₁[k + 1] by A4, XXREAL_0:2; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
hence n |^|^ k > k ; :: thesis: verum