∀ {M : Type u_1} {R : Type u_2} [inst : NonUnitalNonAssocSemiring R] [inst_1 : SetLike M R] [MulMemClass M R] {S : M}
  {a b : R}, a ∈ AddSubmonoid.closure ↑S → b ∈ AddSubmonoid.closure ↑S → a * b ∈ AddSubmonoid.closure ↑S