for k, n being Nat
for th being Real st 0 <= th & th <= 1 & n <= k holds
th |^ k <= th |^ n