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

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then A3: k + 1 < (a |^ k) + 1 by XREAL_1:6;

A4: now :: thesis: not (a |^ k) + 1 > (a |^ k) * a

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:14;
then (((a |^ k) * a1) - 1) + 1 < 0 + 1 by XREAL_1:6;
then ( a |^ k = 0 or a1 = 0 ) by NAT_1:13;
hence contradiction by A1; :: thesis: verum

end;

a |^ (k + 1) = (a |^ k) * a by NEWTON:6;
hence S₁[k + 1] by A3, A4, XXREAL_0:2; :: thesis: verum

end;

A5: S₁[ 0 ] by A1;
for k being Nat holds S₁[k] from NAT_1:sch 2(A5, A2);
hence b < a |^ b ; :: thesis: verum