∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : AddSemigroup M] [inst_2 : ContinuousAdd M] [T2Space M]
  (s : AddSubsemigroup M), (∀ (x y : ↥s), x + y = y + x) → ∀ (x x_1 : ↥s.topologicalClosure), x + x_1 = x_1 + x