agjftucker

import data.set.finite
import topology.instances.real

open set

def is_maximal {α : Type*} [partial_order α] (s : set α) (b : α) : Prop :=
∃ (h : b ∈ s), ∀ b' ∈ s, b ≤ b' → b = b'

lemma exists_maximal {α : Type*} [partial_order α] (s : set α) (hs : finite s) :
  ∀ a ∈ s, ∃ b (h : a ≤ b), is_maximal s b :=