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 A1: ( a >= 1 & n >= 1 ) ; :: thesis: ( n -root a >= 1 & a >= n -root a )
then ( n -Root a >= 1 & a >= n -Root a ) by PREPOWER:38;
hence ( n -root a >= 1 & a >= n -root a ) by A1, Def1; :: thesis: verum