theorem :: POWER:19

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