∀ {R : Type u_1} (M : Type u_1) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
  (r : ↥(AlgebraicGeometry.StructureSheaf.sectionsSubalgebra R U))
  {a : (x : ↥U) → AlgebraicGeometry.StructureSheaf.Localizations M ↑x},
  a ∈ (AlgebraicGeometry.StructureSheaf.sectionsSubmodule M U).carrier →
    ∀ (x : ↥U),
      ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (AlgebraicGeometry.StructureSheaf.isFractionPrelocal R M).pred fun x => (r • a) (i x)