diff --git a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean
index ebae6b3..c762a2e 100644
--- a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean
+++ b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean
@@ -185,7 +185,9 @@ theorem infinitude_of_primes_tfae : [
 
   tfae_have 2 → 3 := by sorry -- Arthur
 
-  tfae_have 1 → 2 := by sorry -- Onat
+  tfae_have 1 → 2 := by -- Onat
+   intro h
+   exact { not_finite := h }
 
   tfae_have 1 → 6 := by sorry -- Bohdan