True ↔ ∃ c, 0 < c ∧ ∀ (K : ℝ), 1 < K → ∃ N₀, ∀ (n : ℕ) (a : Fin n → ℕ), n ≥ N₀ ∧ ∑ i, (↑(a i))⁻¹ > K → ∃ S, 1 - Real.exp (-(c * K)) < ∑ i ∈ S, (↑(a i))⁻¹ ∧ ∑ i ∈ S, (↑(a i))⁻¹ ≤ 1