∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompletePartialOrderSup α] {b : α} [Nonempty ι] {f : ι → α},
  Directed (fun x1 x2 => x1 ≤ x2) f → (∀ (i : ι), f i ≤ b) → (∀ w < b, ∃ i, w < f i) → ⨆ i, f i = b