theorem Th43: :: WALLIS01:43

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