∀ (R : Type u_1) [inst : CommSemiring R] (s x : (TopologicalSpace.Closeds (PrimeSpectrum R))ᵒᵈ),
  PrimeSpectrum.vanishingIdeal s.carrier ≤ PrimeSpectrum.vanishingIdeal ↑(OrderDual.ofDual x) ↔
    ↑(OrderDual.ofDual x) ⊆ s.carrier