∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {E : Type u_3} [inst_2 : EquivLike E α β]
  [OrderIsoClass E α β] (e : E) {s : Set α} [hs : s.OrdConnected], (⇑e '' s).OrdConnected