for k, n being Nat st k < n & 3 <= n & not k + 1 < n holds
2 <= k