no goals
α : Type u_1
β : Type ?u.47637
γ : Type ?u.47640
ι : Sort ?u.47643
inst✝² : ConditionallyCompleteLattice α
s t : Set α
a b : α
inst✝¹ : NoMaxOrder α
inst✝ : DenselyOrdered α
w : α
hw : a < w
⊢ ∃ a_1, a_1 ∈ Ioi a ∧ a_1 < w
simpa using exists_between hw