let a, b be Real; :: thesis: for n being Nat st 0 <= a & a <= b & n >= 1 holds
n -Root a <= n -Root b
let n be Nat; :: thesis: ( 0 <= a & a <= b & n >= 1 implies n -Root a <= n -Root b )
assume that
A1: a >= 0 and
A2: a <= b and
A3: n >= 1 and
A4: n -Root a > n -Root b ; :: thesis: contradiction

A5: now :: thesis: n -Root b >= 0

per cases ( b > 0 or b = 0 ) by A1, A2;

suppose b > 0 ; :: thesis: n -Root b >= 0

hence n -Root b >= 0 by A3, Def2; :: thesis: verum

end;

suppose b = 0 ; :: thesis: n -Root b >= 0

hence n -Root b >= 0 by A3, Def2; :: thesis: verum

end;

end;

end;

(n -Root a) |^ n = a by A1, A3, Th19;
then (n -Root a) |^ n <= (n -Root b) |^ n by A1, A2, A3, Th19;
hence contradiction by A3, A4, A5, Th10; :: thesis: verum