theorem :: POWER:16

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