apply hx
case mp
α : Type u_1
ι : Type u_2
inst✝ : Preorder α
s : ι → α
x : α
hx : x ∈ lowerBounds (Set.range s)
i : ι
⊢ x ≤ s i
case mp.a
α : Type u_1
ι : Type u_2
inst✝ : Preorder α
s : ι → α
x : α
hx : x ∈ lowerBounds (Set.range s)
i : ι
⊢ s i ∈ Set.range s