diff --git a/Analysis/Section_9_4.lean b/Analysis/Section_9_4.lean
index 35affd11..962e6310 100644
--- a/Analysis/Section_9_4.lean
+++ b/Analysis/Section_9_4.lean
@@ -63,7 +63,8 @@ theorem ContinuousWithinAt.tfae (X:Set ℝ) (f: ℝ → ℝ) {x₀:ℝ} (h : x
   [
     ContinuousWithinAt f X x₀,
     ∀ a:ℕ → ℝ, (∀ n, a n ∈ X) → Filter.atTop.Tendsto a (nhds x₀) → Filter.atTop.Tendsto (fun n ↦ f (a n)) (nhds (f x₀)),
-    ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x-x₀| < δ → |f x - f x₀| < ε
+    ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x-x₀| < δ → |f x - f x₀| < ε,
+    ∀ ε > 0, ∃ δ > 0, ∀ x ∈ X, |x-x₀| ≤ δ → |f x - f x₀| ≤ ε
   ].TFAE := by
   sorry