∀ {R : Type u_1} [inst : CommRing R] {S : Type u_1} [inst_1 : CommRing S] {σ : R →+* S}
  (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
  (V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top S)),
  V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier → ∀ (y : ↥V), ↑y ∈ PrimeSpectrum.comap σ ⁻¹' U.carrier