theorem Th7: :: POWER:7
for a being Real
for n being Nat st a >= 0 & n >= 1 holds
n -root a >= 0