∀ {M : Type u_1} [inst : AddZeroClass M] {ι : Type u_4} {p : ι → Prop} {K : ι → AddSubmonoid M} {i : ι},
  p i →
    DirectedOn (Function.onFun (fun x1 x2 => x1 ≤ x2) K) {i | p i} →
      ∀ {x : M}, x ∈ ⨆ i, ⨆ (_ : p i), K i ↔ ∃ i, p i ∧ x ∈ K i