let n be Nat; :: thesis: for r, s being non negative Real st r >= s holds
r |^ n >= s |^ n
let r, s be non negative Real; :: thesis: ( r >= s implies r |^ n >= s |^ n )
( n = 0 implies ( r |^ n = 1 & s |^ n = 1 ) ) by NEWTON:4;
hence ( r >= s implies r |^ n >= s |^ n ) by Th40; :: thesis: verum