theorem Th18: :: POWER:18

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