let a be Real; :: thesis: for n being Nat st a >= 0 & a < 1 & n >= 1 holds
( a <= n -root a & n -root a < 1 )
let n be Nat; :: thesis: ( a >= 0 & a < 1 & n >= 1 implies ( a <= n -root a & n -root a < 1 ) )
assume that
A1: a >= 0 and
A2: a < 1 and
A3: n >= 1 ; :: thesis: ( a <= n -root a & n -root a < 1 )
( a <= n -Root a & n -Root a < 1 ) by A1, A2, A3, PREPOWER:30;
hence ( a <= n -root a & n -root a < 1 ) by A1, A3, Def1; :: thesis: verum