∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrder α] {s : Set α},
  DirectedOn (fun x1 x2 => x1 ≥ x2) s →
    DirectedOn (fun x1 x2 => x1 ≤ x2) s → BddBelow s → BddAbove s → s ⊆ Set.Icc (sInf s) (sSup s)