let a be real number ; :: thesis: for n being Element of NAT st a >= 1 & n >= 1 holds
( n -root a >= 1 & a >= n -root a )
let n be Element of NAT ; :: thesis: ( a >= 1 & n >= 1 implies ( n -root a >= 1 & a >= n -root a ) )
assume that
A1: a >= 1 and
A2: n >= 1 ; :: thesis: ( n -root a >= 1 & a >= n -root a )
( n -Root a >= 1 & a >= n -Root a ) by A1, A2, PREPOWER:38;
hence ( n -root a >= 1 & a >= n -root a ) by A2, Def1; :: thesis: verum