let a be Real; :: thesis: for n being Nat st a >= 1 & n >= 1 holds
( n -root a >= 1 & a >= n -root a )
let n be 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:29;
hence ( n -root a >= 1 & a >= n -root a ) by A2, Def1; :: thesis: verum