∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompletePartialOrderSup α] {f g : ι → α},
  Directed (fun x1 x2 => x1 ≤ x2) f →
    Directed (fun x1 x2 => x1 ≤ x2) g → BddAbove (Set.range g) → (∀ (x : ι), f x ≤ g x) → iSup f ≤ iSup g