no goals
α : Type u_1
β : Type ?u.51575
γ : Type ?u.51578
ι : Sort ?u.51581
inst✝² : ConditionallyCompleteLattice α
s t : Set α
a b : α
inst✝¹ : NoMinOrder α
inst✝ : DenselyOrdered α
w : α
hw : w < a
⊢ ∃ a_1, a_1 ∈ Iio a ∧ w < a_1
simpa [and_comm] using exists_between hw