theorem Th29: :: PREPOWER:29

for a being Real
for n being Nat st a >= 1 & n >= 1 holds
( n -Root a >= 1 & a >= n -Root a )