∀ {ι : Sort u_1} {M : Type u_2} [inst : Add M] (S : ι → AddSubsemigroup M) {C : (x : M) → x ∈ ⨆ i, S i → Prop},
  (∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯) →
    (∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x + y) ⋯) →
      ∀ {x₁ : M} (hx₁ : x₁ ∈ ⨆ i, S i), C x₁ hx₁