False ↔ ∀ (A : Set ℕ), ((∀ᶠ (n : ℕ) in Filter.atTop, ∃ a ∈ A, ∃ b ∈ A, a + b = n) ∧ ∀ (t : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, ∃ pairs, pairs.card ≥ t ∧ ∀ p ∈ pairs, p.1 ∈ A ∧ p.2 ∈ A ∧ p.1 + p.2 = n ∧ p.1 ≤ p.2) → ∃ B C, (∀ (x : ℕ), x ∈ A ↔ x ∈ B ∨ x ∈ C) ∧ Disjoint B C ∧ (∀ᶠ (n : ℕ) in Filter.atTop, ∃ a ∈ B, ∃ b ∈ B, a + b = n) ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∃ a ∈ C, ∃ b ∈ C, a + b = n