for R being commutative Ring
for I being Ideal of R holds
( I is prime iff R / I is domRing ) by Th16, Th17;