no goals
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s : Set (PrimeSpectrum R)
⊢ vanishingIdeal s = ⊤ ↔ s = ∅
rw [← top_le_iff, ← subset_zeroLocus_iff_le_vanishingIdeal, Submodule.top_coe, zeroLocus_univ,
  Set.subset_empty_iff]