>>673
For some n, ∀N [ (n^2 < N ∧ N < n(n+1)) → Comp(N) ]