let a be real number ; :: thesis: for n being Element of NAT st a >= 0 & a < 1 & n >= 1 holds
( a <= n -root a & n -root a < 1 )
let n be Element of NAT ; :: thesis: ( a >= 0 & a < 1 & n >= 1 implies ( a <= n -root a & n -root a < 1 ) )
assume A1: ( a >= 0 & a < 1 & n >= 1 ) ; :: thesis: ( a <= n -root a & n -root a < 1 )
then ( a <= n -Root a & n -Root a < 1 ) by PREPOWER:39;
hence ( a <= n -root a & n -root a < 1 ) by A1, Def1; :: thesis: verum