diff --git a/analysis/Analysis/Section_6_2.lean b/analysis/Analysis/Section_6_2.lean
index b6396b98..66a71b89 100644
--- a/analysis/Analysis/Section_6_2.lean
+++ b/analysis/Analysis/Section_6_2.lean
@@ -168,13 +168,13 @@ example (E: Set EReal) : sSup E < sInf E ↔ E = ∅ := by sorry
 theorem EReal.mem_le_sup (E: Set EReal) {x:EReal} (hx: x ∈ E) : x ≤ sSup E := by sorry
 
 /-- Theorem 6.2.11 (a) / Exercise 6.2.2 -/
-theorem EReal.mem_ge_inf (E: Set EReal) {x:EReal} (hx: x ∈ E) : x ≤ sInf E := by sorry
+theorem EReal.mem_ge_inf (E: Set EReal) {x:EReal} (hx: x ∈ E) : sInf E ≤ x := by sorry
 
 /-- Theorem 6.2.11 (b) / Exercise 6.2.2 -/
 theorem EReal.sup_le_upper (E: Set EReal) {M:EReal} (hM: M ∈ upperBounds E) : sSup E ≤ M := by sorry
 
 /-- Theorem 6.2.11 (c) / Exercise 6.2.2 -/
-theorem EReal.inf_ge_upper (E: Set EReal) {M:EReal} (hM: M ∈ upperBounds E) : sInf E ≥ M := by sorry
+theorem EReal.inf_ge_upper (E: Set EReal) {M:EReal} (hM: M ∈ lowerBounds E) : sInf E ≥ M := by sorry
 
 #check isLUB_iff_sSup_eq
 #check isGLB_iff_sInf_eq