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 >= n -Root 1 by Th36;
hence n -Root a >= 1 by A1, Th29; :: thesis: a >= n -Root a
n -Root a <= n -Root (a |^ n) by A1, Th20, Th36;
hence a >= n -Root a by A1, Lm2; :: thesis: verum