∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β] {f : α → β},
  OmegaCompletePartialOrder.ωScottContinuous f →
    ∃ (hf : Monotone f),
      ∀ (c : OmegaCompletePartialOrder.Chain α),
        f (OmegaCompletePartialOrder.ωSup c) = OmegaCompletePartialOrder.ωSup (c.map { toFun := f, monotone' := hf })