∀ {𝕜 : Type u_1} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] {E : Type u_2} [inst_2 : AddCommMonoid E]
  [inst_3 : TopologicalSpace E] [inst_4 : SMul 𝕜 E] [ContinuousConstSMul 𝕜 E] (K : ConvexCone 𝕜 E) (c : 𝕜),
  0 < c → ∀ x ∈ closure ↑K, c • x ∈ closure ↑K