{α : Type u_2} →
  [toPartialOrder : PartialOrder α] →
    (cSup : NonemptyChain α → α) →
      (∀ (c : NonemptyChain α), ∀ x ∈ c.carrier, x ≤ cSup c) →
        (∀ (c : NonemptyChain α) (x : α), (∀ y ∈ c.carrier, y ≤ x) → cSup c ≤ x) → ChainCompletePartialOrder α