theorem Th40: :: WALLIS01:2

for n, m being Nat
for x being Real st n < m & 0 < x & x < 1 holds
x |^ m < x |^ n