∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : ConditionallyCompleteLattice β] {f : α → β},
  Monotone f → ∀ {s : Set α}, s.Nonempty → ∀ {B : α}, B ∈ upperBounds s → sSup (f '' s) ≤ f B