Totally_Ordered_Set_is_Lattice

import Mathlib.Order.Lattice

theorem Totally_Ordered_Set_is_Lattice {α : Type _} [LinearOrder α] (a b : α) : ∃ c : α, a ≤ c ∧ b ≤ c ∧ ∀ d, a ≤ d → b ≤ d → c ≤ d := by sorry