let a be Nat; :: thesis: for b being non trivial Nat ex n being Nat st a < b |^ n
let b be non trivial Nat; :: thesis: ex n being Nat st a < b |^ n
reconsider d = log (b,(a + 1)) as Real ;
reconsider c = [/d\] as Integer ;
A1: ( b >= 1 & d <= [/d\] ) by INT_1:def 7, NEWTON03:def 1;
then A2: b to_power d <= b to_power [/d\] by PRE_FF:8;
a + 0 < a + 1 by XREAL_1:6;
then A3: a < b to_power c by A2, XXREAL_0:2;

per cases ( c <= 0 or c > 0 ) ;

suppose c <= 0 ; :: thesis: ex n being Nat st a < b |^ n

then b to_power c <= b to_power 0 by A1, PRE_FF:8;
then a < b to_power 0 by A3, XXREAL_0:2;
hence ex n being Nat st a < b |^ n ; :: thesis: verum

end;

suppose c > 0 ; :: thesis: ex n being Nat st a < b |^ n

then c in NAT by INT_1:3;
then reconsider c = c as Nat ;
a < b |^ c by A3, POWER:41;
hence ex n being Nat st a < b |^ n ; :: thesis: verum

end;

end;