no goals
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
s t : Set (PrimeSpectrum R)
hs : IsClosed s
ht : IsClosed t
⊢ s ⊂ t ↔ vanishingIdeal t < vanishingIdeal s
rw [Set.ssubset_def, vanishingIdeal_anti_mono_iff hs, vanishingIdeal_anti_mono_iff ht,
  lt_iff_le_not_le]