theorem Th47: :: WALLIS01:47

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