∀ {α : Type u_2} {β : Type u_3} {a : α} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {f : α → β},
  a ∈ s →
    (∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)) →
      (Maximal (fun x => x ∈ f '' s) (f a) ↔ Maximal (fun x => x ∈ s) a)