∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} {I : PrimeSpectrum (Polynomial R)},
  I ∈ (PrimeSpectrum.zeroLocus {f})ᶜ → PrimeSpectrum.comap Polynomial.C I ∈ AlgebraicGeometry.Polynomial.imageOfDf f