theorem :: POWER:21

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