theorem Th6: :: NAT_4:6

for n being Nat holds (2 * n) choose n >= (4 |^ n) / (2 * n)