∀ {K : Type u_1} [inst : Field K] [inst_1 : ValuativeRel K] [inst_2 : TopologicalSpace K],
  (∀ {s : Set K} {x : K}, s ∈ nhds x ↔ ∃ γ, (fun x_1 => x + x_1) '' {z | (ValuativeRel.valuation K) z < ↑γ} ⊆ s) →
    (∀ (x : K), ∀ n ∈ nhds x, ∃ s ∈ nhds x, s ⊆ n ∧ IsCompact s) → (∃ γ, γ ≠ 0 ∧ γ ≠ 1) → IsNonarchimedeanLocalField K