∀ (R : Type u_1) [inst : CommRing R] (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
  (x : ↥(Opposite.unop (Opposite.op U))),
  ∃ V,
    ∃ (_ : ↑x ∈ V),
      ∃ i,
        (AlgebraicGeometry.StructureSheaf.isFractionPrelocal R).pred fun x =>
          (algebraMap R (AlgebraicGeometry.StructureSheaf.Localizations R ↑(i x))) 1