∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [IsLocalization M S] [IsDomain R],
  M ≤ nonZeroDivisors R → ∀ (p : Ideal S) [hpp : p.IsPrime], p ≠ ⊥ → ⊥ < Ideal.comap (algebraMap R S) p