theorem Th46: :: WALLIS01:46

for n being non zero Nat holds ('I' . (2 * n)) / ('I' . ((2 * n) + 1)) <= 1 + (1 / (2 * n))