intro s x
X : Type u_1
inst✝ : PartialOrder X
I : Set X → X
h : isInfFun I
⊢ isSupFun fun s => I (upperBounds s)
X : Type u_1
inst✝ : PartialOrder X
I : Set X → X
h : isInfFun I
s : Set X
x : X
⊢ x ∈ upperBounds s ↔ (fun s => I (upperBounds s)) s ≤ x