{α : Type u_5} →
  (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) →
            (sup : α → α → α) →
              (∀ (a b : α), le a (sup a b)) →
                (∀ (a b : α), le b (sup a b)) →
                  (∀ (a b c : α), le a c → le b c → le (sup a b) c) →
                    (inf : α → α → α) →
                      (∀ (a b : α), le (inf a b) a) →
                        (∀ (a b : α), le (inf a b) b) →
                          (∀ (a b c : α), le a b → le a c → le a (inf b c)) →
                            (sSup sInf : Set α → α) →
                              (∀ (s : Set α) (a : α), BddAbove s → a ∈ s → le a (sSup s)) →
                                (∀ (s : Set α) (a : α), s.Nonempty → a ∈ upperBounds s → le (sSup s) a) →
                                  (∀ (s : Set α) (a : α), BddBelow s → a ∈ s → le (sInf s) a) →
                                    (∀ (s : Set α) (a : α), s.Nonempty → a ∈ lowerBounds s → le a (sInf s)) →
                                      ConditionallyCompleteLattice α