theorem Th41: :: WALLIS01:3

for n being non zero Nat
for x being Real st 0 < x & x < PI / 2 holds
( (sin . x) |^ (2 * n) < (sin . x) |^ ((2 * n) -' 1) & (sin . x) |^ ((2 * n) + 1) < (sin . x) |^ (2 * n) )