theorem :: NEWTON02:123

for b being Nat holds (b + 1) ! >= 2 |^ b