let a be positive Real; :: thesis: for n being positive Nat holds n -root a is positive
let n be positive Nat; :: thesis: n -root a is positive
I1: n -root a <> 0

proof

assume n -root a = 0 ; :: thesis: contradiction
then (n -root a) |^ n = 0 |^ n ;
hence contradiction ; :: thesis: verum

end;

n >= 1 + 0 by NAT_1:13;
hence n -root a is positive by I1, POWER:7; :: thesis: verum