let R be domRing; :: thesis: {(0. R)} is prime

not 1_ R in {(0. R)} by TARSKI:def 1;

hence {(0. R)} is proper by IDEAL_1:19; :: according to RING_1:def 2 :: thesis: {(0. R)} is quasi-prime

let a, b be Element of R; :: according to RING_1:def 1 :: thesis: ( not a * b in {(0. R)} or a in {(0. R)} or b in {(0. R)} )

assume a * b in {(0. R)} ; :: thesis: ( a in {(0. R)} or b in {(0. R)} )

then a * b = 0. R by TARSKI:def 1;

then ( a = 0. R or b = 0. R ) by VECTSP_2:def 1;

hence ( a in {(0. R)} or b in {(0. R)} ) by TARSKI:def 1; :: thesis: verum

not 1_ R in {(0. R)} by TARSKI:def 1;

hence {(0. R)} is proper by IDEAL_1:19; :: according to RING_1:def 2 :: thesis: {(0. R)} is quasi-prime

let a, b be Element of R; :: according to RING_1:def 1 :: thesis: ( not a * b in {(0. R)} or a in {(0. R)} or b in {(0. R)} )

assume a * b in {(0. R)} ; :: thesis: ( a in {(0. R)} or b in {(0. R)} )

then a * b = 0. R by TARSKI:def 1;

then ( a = 0. R or b = 0. R ) by VECTSP_2:def 1;

hence ( a in {(0. R)} or b in {(0. R)} ) by TARSKI:def 1; :: thesis: verum