let n be Nat; for a being Nat ex b being Nat st
( b |^ (n + 1) <= a & a < (b + 1) |^ (n + 1) )
defpred S1[ Nat] means ex b being Nat st
( b |^ (n + 1) <= $1 & $1 < (b + 1) |^ (n + 1) );
A1:
S1[ 0 ]
A2:
for k being Nat st S1[k] holds
S1[k + 1]
for x being Nat holds S1[x]
from NAT_1:sch 2(A1, A2);
hence
for a being Nat ex b being Nat st
( b |^ (n + 1) <= a & a < (b + 1) |^ (n + 1) )
; verum