diff --git a/src/order/zorn.lean b/src/order/zorn.lean
index 2804ab41623b0..7318858d40674 100644
--- a/src/order/zorn.lean
+++ b/src/order/zorn.lean
@@ -129,6 +129,13 @@ begin
       exact ⟨z, ⟨hzs, (hcs hy).2.trans $ hz _ hy⟩, hz⟩ } }
 end
 
+lemma zorn_nonempty_Ici₀ (a : α)
+  (ih : ∀ c ⊆ Ici a, is_chain (≤) c → ∀ y ∈ c, ∃ ub, a ≤ ub ∧ ∀ z ∈ c, z ≤ ub) (x : α)
+  (hax : a ≤ x) :
+  ∃ m, x ≤ m ∧ ∀ z, m ≤ z → z ≤ m :=
+let ⟨m, hma, hxm, hm⟩ := zorn_nonempty_preorder₀ (Ici a) (by simpa using ih) x hax in
+  ⟨m, hxm, λ z hmz, hm _ (hax.trans $ hxm.trans hmz) hmz⟩
+
 end preorder
 
 section partial_order