let a, b be natural number ; :: thesis: ( 1 < a implies b <= a |^ b )
assume A1: 1 < a ; :: thesis: b <= a |^ b
then reconsider a1 = a - 1 as Element of NAT by INT_1:18;
defpred S₁[ natural number ] means $1 <= a |^ $1;
A2: S₁[ 0 ] ;
A3: for k being natural number st S₁[k] holds
S₁[k + 1]

proof

let k be natural number ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
A5: k + 1 <= (a |^ k) + 1 by A4, XREAL_1:8;
A6: a |^ (k + 1) = (a |^ k) * a by NEWTON:11;

now

set x = a |^ k;
assume (a |^ k) + 1 > (a |^ k) * a ; :: thesis: contradiction
then ((a |^ k) * a) - ((a |^ k) + 1) < ((a |^ k) + 1) - ((a |^ k) + 1) by XREAL_1:16;
then (((a |^ k) * a1) - 1) + 1 < 0 + 1 by XREAL_1:8;
then (a |^ k) * a1 <= 0 by NAT_1:13;
then (a |^ k) * a1 = 0 ;
then ( a |^ k = 0 or a1 = 0 ) ;
hence contradiction by A1; :: thesis: verum

end;

hence k + 1 <= a |^ (k + 1) by A5, A6, XXREAL_0:2; :: thesis: verum

end;

for k being natural number holds S₁[k] from NAT_1:sch 2(A2, A3);
hence b <= a |^ b ; :: thesis: verum