let n be non zero Nat; :: thesis: for a being non negative Real st a > 1 holds
n -root a > 1
let a be non negative Real; :: thesis: ( a > 1 implies n -root a > 1 )
assume A1: a > 1 ; :: thesis: n -root a > 1
n >= 1 by NAT_1:14;
then n -root a > n -root 1 by A1, POWER:17;
hence n -root a > 1 ; :: thesis: verum