theorem Th22: :: POWER:22

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