theorem Th27: :: PREPOWER:27

for a, b being Real
for n being Nat st 0 <= a & a <= b & n >= 1 holds
n -Root a <= n -Root b