∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddCommGroup α] {s : Set α} (x : α)
  (motive : x ∈ LatticeOrderedAddCommGroup.solidClosure s → Prop) (x_1 : x ∈ LatticeOrderedAddCommGroup.solidClosure s),
  (∀ (w : α) (hy : w ∈ s) (hxy : |x| ≤ |w|), motive ⋯) → motive x_1