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₁[ Nat] means ex b being Nat st
( b |^ (n + 1) <= $1 & $1 < (b + 1) |^ (n + 1) );
A1: S₁[ 0 ]

proof

( 0 |^ (n + 1) <= 0 & 0 < (0 + 1) |^ (n + 1) ) ;
hence S₁[ 0 ] ; :: thesis: verum

end;

A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[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;

per cases then ( k + 1 < (b + 1) |^ (n + 1) or k + 1 = (b + 1) |^ (n + 1) ) by XXREAL_0:1;

suppose A5: k + 1 < (b + 1) |^ (n + 1) ; :: thesis: S₁[k + 1]

k + 1 > b |^ (n + 1) by A3, NAT_1:13;
hence S₁[k + 1] by A5; :: thesis: verum

end;

suppose A5: k + 1 = (b + 1) |^ (n + 1) ; :: thesis: S₁[k + 1]

then k + 1 < ((b + 1) + 1) |^ (n + 1) by A4, Th40;
hence S₁[k + 1] by A5; :: thesis: verum

end;

end;

end;

for x being Nat holds S₁[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