diff --git a/analysis/Analysis/Section_6_4.lean b/analysis/Analysis/Section_6_4.lean
index 360cdfc9..8bff023a 100644
--- a/analysis/Analysis/Section_6_4.lean
+++ b/analysis/Analysis/Section_6_4.lean
@@ -299,7 +299,7 @@ theorem Sequence.Cauchy_iff_convergent (a:Sequence) :
   grind
 
 /-- Exercise 6.4.6 -/
-theorem Sequence.sup_not_strict_mono : ∃ (a b:ℕ → ℝ), (∀ n, a n < b n) ∧ (a:Sequence).sup ≠ (b:Sequence).sup := by
+theorem Sequence.sup_not_strict_mono : ∃ (a b:ℕ → ℝ), (∀ n, a n < b n) ∧ ¬ (a:Sequence).sup < (b:Sequence).sup := by
   sorry
 
 /- Exercise 6.4.7 -/