∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] {α : Type u_3} {β : Type u_4} [Countable β]
  [inst_3 : CompleteLattice α] (m : α → M),
  m ⊥ = 0 →
    ∀ (R : M → M → Prop),
      (∀ (s : ℕ → α), R (m (⨆ i, s i)) (∑' (i : ℕ), m (s i))) → ∀ (s : β → α), R (m (⨆ b, s b)) (∑' (b : β), m (s b))