theorem Th17: :: POWER:17

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