∀ (α : Type u_1) [H1 : PartialOrder α] [H2 : SupSet α] (bddAbove_pair : ∀ (a b : α), BddAbove {a, b})
  (bddBelow_pair : ∀ (a b : α), BddBelow {a, b})
  (isLUB_sSup : ∀ (s : Set α), BddAbove s → s.Nonempty → IsLUB s (sSup s)) (x : Set α),
  x.Nonempty → BddBelow x → IsGLB x (sSup (lowerBounds x))