diff --git a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean
index ebae6b3..d610a01 100644
--- a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean
+++ b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean
@@ -197,7 +197,9 @@ theorem infinitude_of_primes_tfae : [
   
   tfae_have 6 → 3 := by sorry -- Anna
 
-  tfae_have 6 → 1 := by sorry -- Alexander
+  tfae_have 6 → 1 := by -- Alexander
+   rintro ⟨P, hP, hprime⟩
+   exact Set.infinite_of_injective_forall_mem hP (fun x => hprime x)
 
   tfae_have 4 → 1 := by sorry -- Cara