theorem Th30: :: PREPOWER:30

for a being Real
for n being Nat st 0 <= a & a < 1 & n >= 1 holds
( a <= n -Root a & n -Root a < 1 )