Subset_of_Well_Ordered_Set_is_Well_Ordered

import Mathlib.Order.WellFounded
import Mathlib.Data.Set.Basic
import Mathlib.Order.Basic

theorem Subset_of_Well_Ordered_Set_is_Well_Ordered {α : Type _} [LinearOrder α] [IsWellOrder α (· < ·)] (S : Set α) (hS : S.Nonempty) : ∃ m ∈ S, ∀ x ∈ S, m ≤ x := by sorry