∀ {α : Type u_1} [inst : SemilatticeInf α] {T : Set α} [OrderTop α] [inst_2 : TopologicalSpace α] [Topology.IsLower α],
  (∀ p ∈ T, InfPrime p) → TopologicalSpace.IsTopologicalBasis {S | ∃ a, (PrimitiveSpectrum.hull T a)ᶜ = S}