∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (p : Seminorm 𝕜 E) {c : 𝕜},
  1 < ‖c‖ →
    ∀ {ε : ℝ}, 0 < ε → ∀ {x : E}, p x ≠ 0 → ∃ d, d ≠ 0 ∧ p (d • x) < ε ∧ ε / ‖c‖ ≤ p (d • x) ∧ ‖d‖⁻¹ ≤ ε⁻¹ * ‖c‖ * p x