∀ {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [SMulCommClass R R M] (s t : Set R) (x : Submodule R M) (r : R) (m : M), r ∈ s → m ∈ t • x → r • m ∈ (s * t) • x