let m be Nat; :: thesis: for r being Real st m > 1 holds
ex n being positive Nat st m |^ (m |^ n) > r
let r be Real; :: thesis: ( m > 1 implies ex n being positive Nat st m |^ (m |^ n) > r )
assume A1: m > 1 ; :: thesis: ex n being positive Nat st m |^ (m |^ n) > r

per cases ( r > 1 or r <= 1 ) ;

suppose A2: r > 1 ; :: thesis: ex n being positive Nat st m |^ (m |^ n) > r

set L = log (m,r);
set n = [/(log (m,r))\];
A3: log (m,r) <= [/(log (m,r))\] by INT_1:def 7;
log (m,r) > 0 by A1, A2, ENTROPY1:4;
then reconsider n = [/(log (m,r))\] as positive Nat by TARSKI:1;
take n ; :: thesis: m |^ (m |^ n) > r
A4: m to_power (log (m,r)) <= m to_power n by A1, A3, PRE_FF:8;
A5: m to_power (log (m,r)) = r by A1, A2, POWER:def 3;
m |^ n < m |^ (m |^ n) by A1, NAT_3:2;
hence m |^ (m |^ n) > r by A4, A5, XXREAL_0:2; :: thesis: verum

end;

suppose A6: r <= 1 ; :: thesis: ex n being positive Nat st m |^ (m |^ n) > r

take 1 ; :: thesis: m |^ (m |^ 1) > r
A7: m |^ m > m |^ 1 by A1, PEPIN:66;
r < m by A1, A6, XXREAL_0:2;
hence m |^ (m |^ 1) > r by A7, XXREAL_0:2; :: thesis: verum

end;

end;