{α : Type u_3} →
  (le lt : α → α → Prop) →
    (∀ (a : α), le a a) →
      (∀ (a b c : α), le a b → le b c → le a c) →
        autoParam (∀ (a b : α), lt a b ↔ le a b ∧ ¬le b a) Preorder.lt_iff_le_not_ge._autoParam →
          (∀ (a b : α), le a b → le b a → a = b) →
            (sSup : Set α → α) →
              (∀ (s : Set α), DirectedOn (fun x1 x2 => le x1 x2) s → s.Nonempty → BddAbove s → IsLUB s (sSup s)) →
                (sInf : Set α → α) →
                  (∀ (s : Set α), DirectedOn (fun x1 x2 => x1 ≥ x2) s → s.Nonempty → BddBelow s → IsGLB s (sInf s)) →
                    ConditionallyCompletePartialOrder α