theorem Th20: :: POWER:20

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