let n, m be Nat; :: thesis: for x being Real st n < m & 0 < x & x < 1 holds
x |^ m < x |^ n
let x be Real; :: thesis: ( n < m & 0 < x & x < 1 implies x |^ m < x |^ n )
assume ( n < m & 0 < x & x < 1 ) ; :: thesis: x |^ m < x |^ n
then x to_power n > x to_power m by POWER:40;
hence x |^ m < x |^ n ; :: thesis: verum