{α : Type u_8} →
  {P : Sort u} →
    {toPartialOrder : PartialOrder α} →
      {toSupSet : SupSet α} →
        {le_sSup : ∀ (s : Set α), ∀ a ∈ s, a ≤ sSup s} →
          {sSup_le : ∀ (s : Set α) (a : α), (∀ b ∈ s, b ≤ a) → sSup s ≤ a} →
            {toPartialOrder' : PartialOrder α} →
              {toSupSet' : SupSet α} →
                {le_sSup' : ∀ (s : Set α), ∀ a ∈ s, a ≤ sSup s} →
                  {sSup_le' : ∀ (s : Set α) (a : α), (∀ b ∈ s, b ≤ a) → sSup s ≤ a} →
                    { toPartialOrder := toPartialOrder, toSupSet := toSupSet, le_sSup := le_sSup, sSup_le := sSup_le } =
                        { toPartialOrder := toPartialOrder', toSupSet := toSupSet', le_sSup := le_sSup',
                          sSup_le := sSup_le' } →
                      (toPartialOrder ≍ toPartialOrder' → toSupSet ≍ toSupSet' → P) → P