diff --git a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean
index ebae6b3..cd3505e 100644
--- a/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean
+++ b/LeanBlockCourse26/P06_Mathlib/S01_PrimeTheorem.lean
@@ -201,7 +201,10 @@ theorem infinitude_of_primes_tfae : [
 
   tfae_have 4 → 1 := by sorry -- Cara
 
-  tfae_have 1 → 5 := by sorry -- Tonio
+  tfae_have 1 → 5 := by -- Tonio
+   intro h n
+   have ⟨x, y, z⟩ := h.exists_gt n
+   exact ⟨x, z, y⟩
 
   tfae_have 1 → 3 := by sorry -- Nina