∀ {α : Type u_6} {β : Type u_7} {inst : Preorder α} {inst_1 : Preorder β} {inst_2 : BoundedOrder α}
  {inst_3 : BoundedOrder β} {toOrderHom : α →o β} {map_top' : toOrderHom.toFun ⊤ = ⊤}
  {map_bot' : toOrderHom.toFun ⊥ = ⊥} {toOrderHom_1 : α →o β} {map_top'_1 : toOrderHom_1.toFun ⊤ = ⊤}
  {map_bot'_1 : toOrderHom_1.toFun ⊥ = ⊥},
  { toOrderHom := toOrderHom, map_top' := map_top', map_bot' := map_bot' } =
      { toOrderHom := toOrderHom_1, map_top' := map_top'_1, map_bot' := map_bot'_1 } →
    toOrderHom = toOrderHom_1