let n be Nat; :: thesis: for a being Nat ex b being Nat st

( b |^ (n + 1) <= a & a < (b + 1) |^ (n + 1) )

defpred S_{1}[ Nat] means ex b being Nat st

( b |^ (n + 1) <= $1 & $1 < (b + 1) |^ (n + 1) );

A1: S_{1}[ 0 ]
A2:
for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[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) ) ; :: thesis: verum

( b |^ (n + 1) <= a & a < (b + 1) |^ (n + 1) )

defpred S

( b |^ (n + 1) <= $1 & $1 < (b + 1) |^ (n + 1) );

A1: S

S

proof

for x being Nat holds S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume S_{1}[k]
; :: thesis: S_{1}[k + 1]

then consider b being Nat such that

A3: ( b |^ (n + 1) <= k & k < (b + 1) |^ (n + 1) ) ;

A4: ( b + 1 > b + 0 & (b + 1) + 1 > (b + 1) + 0 ) by XREAL_1:6;

k + 1 <= (b + 1) |^ (n + 1) by A3, NAT_1:13;

end;assume S

then consider b being Nat such that

A3: ( b |^ (n + 1) <= k & k < (b + 1) |^ (n + 1) ) ;

A4: ( b + 1 > b + 0 & (b + 1) + 1 > (b + 1) + 0 ) by XREAL_1:6;

k + 1 <= (b + 1) |^ (n + 1) by A3, NAT_1:13;

hence for a being Nat ex b being Nat st

( b |^ (n + 1) <= a & a < (b + 1) |^ (n + 1) ) ; :: thesis: verum