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