∀ {R : Type u_1} [inst : Mul R] [inst_1 : StarMul R] {s : Set R},
  (∀ x ∈ s, ∀ y ∈ s, y * x = x * y) →
    (∀ x ∈ s, ∀ y ∈ s, y * star x = star x * y) → ∀ x ∈ s ∪ star s, ∀ y ∈ s ∪ star s, y * x = x * y