∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {s : Set A}
  {p : (x : A) → x ∈ Algebra.adjoin R s → Prop},
  (∀ (x : A) (hx : x ∈ s), p x ⋯) →
    (∀ (r : R), p ((algebraMap R A) r) ⋯) →
      (∀ (x y : A) (hx : x ∈ Algebra.adjoin R s) (hy : y ∈ Algebra.adjoin R s), p x hx → p y hy → p (x + y) ⋯) →
        (∀ (x y : A) (hx : x ∈ Algebra.adjoin R s) (hy : y ∈ Algebra.adjoin R s), p x hx → p y hy → p (x * y) ⋯) →
          ∀ {x : A} (hx : x ∈ Algebra.adjoin R s), p x hx