theorem Th45: :: WALLIS01:45

for n being non zero Nat holds 1 / ((1 + (1 / (2 * n))) * PI) <= (((Product (odd-seq n)) |^ 2) / ((Product (even-seq n)) |^ 2)) * n