theorem PositiveRoot: :: NUMBER12:60

for a being positive Real
for n being positive Nat holds n -root a is positive