Erdős Problem 312

Reference: erdosproblems.com/312

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

Does there exist a constant c > 0 such that, for any K > 1, whenever A is a sufficiently large finite multiset of integers with $\sum_{n \in A} 1/n > K$ there exists some $S \subseteq A$ such that $1 - \exp(-(c*K)) < \sum_{n \in S} 1/n \le 1$?