let R be commutative Ring; :: thesis: for I being Ideal of R holds
( I is prime iff R / I is domRing )
let I be Ideal of R; :: thesis: ( I is prime iff R / I is domRing )
thus ( I is prime implies R / I is domRing ) by Th16, Th17; :: thesis: ( R / I is domRing implies I is prime )
assume R / I is domRing ; :: thesis: I is prime
hence ( I is proper & I is quasi-prime ) by Th16, Th17; :: according to RING_1:def 2 :: thesis: verum