False ↔ ∀ (A : Set ℕ), A.IsAsymptoticAddBasisOfOrder 2 → Filter.Tendsto (fun n => Erdos868.ncard_add_repr A 2 n) Filter.atTop Filter.atTop → ∃ B ⊆ A, B.IsAsymptoticAddBasisOfOrder 2 ∧ ∀ b ∈ B, ¬(B \ {b}).IsAsymptoticAddBasisOfOrder 2