∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {s : Set 𝕜} [CompactSpace ↑s] {p : C(↑s, 𝕜) → Prop},
  (∀ (r : 𝕜), p (ContinuousMap.const (↑s) r)) →
    p (ContinuousMap.restrict s (ContinuousMap.id 𝕜)) →
      p (star (ContinuousMap.restrict s (ContinuousMap.id 𝕜))) →
        (∀ (f g : C(↑s, 𝕜)), p f → p g → p (f + g)) →
          (∀ (f g : C(↑s, 𝕜)), p f → p g → p (f * g)) →
            (∀ (f : C(↑s, 𝕜)), (∃ᶠ (g : C(↑s, 𝕜)) in nhds f, p g) → p f) → ∀ (f : C(↑s, 𝕜)), p f