let n be non zero Nat; :: thesis: 0 < 'I' . ((2 * n) -' 1)
set evenn = Product (even-seq n);
set oddn = Product (odd-seq n);
'I' . (2 * n) = ((Product (odd-seq n)) / (Product (even-seq n))) * (PI / 2) by Th38;
hence 0 < 'I' . ((2 * n) -' 1) by Th43, COMPTRIG:5; :: thesis: verum