for n being Nat st n >= 1 holds
2 <= (n + 1) !