Composite_of_Order_Isomorphisms_is_Order_Isomorphism

import Mathlib.Order.Hom.Basic

theorem Composite_of_Order_Isomorphisms_is_Order_Isomorphism {α : Type _} {β : Type _} {γ : Type _} [Preorder α] [Preorder β] [Preorder γ] (φ : α ≃o β) (ψ : β ≃o γ) : Nonempty (α ≃o γ) := by sorry