theorem Th42: :: WALLIS01:42

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