diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 0d911f46c..b7fcc4b73 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -3,6 +3,9 @@
 ## [Unreleased]
 
 ### Added
+- in order_topology.v
+  + lemma `itv_closed_ends_closed`
+
 - in set_interval.v
   + definitions `itv_is_closed_unbounded`, `itv_is_cc`, `itv_closed_ends`
 
@@ -10,6 +13,9 @@
   + lemma `RlnE`
 
 ### Changed
+- in set_interval.v
+  + `itv_is_closed_unbounded` (fix the definition)
+
 - in set_interval.v
   + `itv_is_open_unbounded`, `itv_is_oo`, `itv_open_ends` (Prop to bool)
 
diff --git a/classical/set_interval.v b/classical/set_interval.v
index 3f21bbf46..7008aadd0 100644
--- a/classical/set_interval.v
+++ b/classical/set_interval.v
@@ -850,7 +850,7 @@ Implicit Types (i : interval T).
 
 Definition itv_is_closed_unbounded i : bool :=
   match i with
-  | `[_, +oo[ | `]-oo, _[ | `]-oo, +oo[ => true
+  | `[_, +oo[ | `]-oo, _] | `]-oo, +oo[ => true
   | _ => false
   end.
 
diff --git a/theories/topology_theory/order_topology.v b/theories/topology_theory/order_topology.v
index 0658f12ce..eafb9197a 100644
--- a/theories/topology_theory/order_topology.v
+++ b/theories/topology_theory/order_topology.v
@@ -111,6 +111,10 @@ Lemma itv_closed x y : @closed T `[x, y].
 Proof. by rewrite set_itv_splitI; apply: closedI => /=. Qed.
 Hint Resolve itv_closed : core.
 
+Lemma itv_closed_ends_closed (i : interval T) :
+  itv_closed_ends i -> closed [set` i].
+Proof. by case: i => [[[]t1|[]]] [[]t2|[]]. Qed.
+
 Lemma itv_closure x y : closure `]x, y[ `<=` `[x, y].
 Proof.
 rewrite closureE => r; apply; split => //.