∀ {α : Type u_1} [inst : PartialOrder α] (s : Set α) (b : α) (hb : b ∈ s) (motive : (x : ↑s) → ⟨b, hb⟩ ≤ x → Prop)
  (x : ↑s) (hbc : ⟨b, hb⟩ ≤ x), (∀ (c : α) (hc : c ∈ s) (hbc : ⟨b, hb⟩ ≤ ⟨c, hc⟩), motive ⟨c, hc⟩ hbc) → motive x hbc