∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
  {f : α →o β},
  (∀ (c : OmegaCompletePartialOrder.Chain α),
      f (OmegaCompletePartialOrder.ωSup c) = OmegaCompletePartialOrder.ωSup (c.map f)) →
    OmegaCompletePartialOrder.ωScottContinuous ⇑f