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

A3: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
succ (Segm k) = Segm (k + 1) by NAT_1:38;
then n |^|^ (k + 1) = exp (n,(n |^|^ k)) by Th14
.= n |^ (n |^|^ k) ;
then A5: n |^|^ (k + 1) > n |^ k by A1, A4, PEPIN:66;
n |^ k > k by A1, NAT_4:3;
then n |^ k >= k + 1 by NAT_1:13;
hence S₁[k + 1] by A5, XXREAL_0:2; :: thesis: verum

end;

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