let m be Nat; :: thesis: ( 2 <= m implies for A being Real ex n being positive Nat st A <= m |^ n )
assume 2 <= m ; :: thesis: for A being Real ex n being positive Nat st A <= m |^ n
then 1 + 1 <= m ;
then A1: 1 < m by NAT_1:13;
let A be Real; :: thesis: ex n being positive Nat st A <= m |^ n
reconsider a = |.[/A\].| as Nat by TARSKI:1;
reconsider n = a + 1 as positive Nat ;
( A <= [/A\] & [/A\] <= a ) by ABSVALUE:4, INT_1:def 7;
then A2: A <= a by XXREAL_0:2;
( a < n & n <= m |^ n ) by A1, NAT_3:2, NAT_1:13;
then a <= m |^ n by XXREAL_0:2;
hence ex n being positive Nat st A <= m |^ n by A2, XXREAL_0:2; :: thesis: verum