let n be Nat; :: thesis: 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 ]
proof
( 0 |^ (n + 1) <= 0 & 0 < (0 + 1) |^ (n + 1) ) ;
hence S1[ 0 ] ; :: thesis: verum
end;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume S1[k] ; :: thesis: S1[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 ;
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: S1[k + 1]
k + 1 > b |^ (n + 1) by ;
hence S1[k + 1] by A5; :: thesis: verum
end;
suppose A5: k + 1 = (b + 1) |^ (n + 1) ; :: thesis: S1[k + 1]
then k + 1 < ((b + 1) + 1) |^ (n + 1) by ;
hence S1[k + 1] by A5; :: thesis: verum
end;
end;
end;
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) ) ; :: thesis: verum