let R be Ring; :: thesis: for I being Ideal of R holds
( I is quasi-prime iff R / I is domRing-like )
let I be Ideal of R; :: thesis: ( I is quasi-prime iff R / I is domRing-like )
set E = EqRel R,I;
A1: Class (EqRel R,I),(0. R) = 0. (R / I) by Def6;
thus ( I is quasi-prime implies R / I is domRing-like ) :: thesis: ( R / I is domRing-like implies I is quasi-prime )

proof

assume A2: I is quasi-prime ; :: thesis: R / I is domRing-like
let x, y be Element of (R / I); :: according to VECTSP_2:def 5 :: thesis: ( not x * y = 0. (R / I) or x = 0. (R / I) or y = 0. (R / I) )
assume A3: x * y = 0. (R / I) ; :: thesis: ( x = 0. (R / I) or y = 0. (R / I) )
consider a being Element of R such that
A4: x = Class (EqRel R,I),a by Th11;
consider b being Element of R such that
A5: y = Class (EqRel R,I),b by Th11;
x * y = Class (EqRel R,I),(a * b) by A4, A5, Th14;
then ( (a * b) - (0. R) = a * b & (a * b) - (0. R) in I ) by A1, A3, Th6, RLVECT_1:26;
then A6: ( a in I or b in I ) by A2, Def1;
( a - (0. R) = a & b - (0. R) = b ) by RLVECT_1:26;
hence ( x = 0. (R / I) or y = 0. (R / I) ) by A1, A4, A5, A6, Th6; :: thesis: verum

end;

assume A7: R / I is domRing-like ; :: thesis: I is quasi-prime
let a, b be Element of R; :: according to RING_1:def 1 :: thesis: ( not a * b in I or a in I or b in I )
reconsider x = Class (EqRel R,I),a, y = Class (EqRel R,I),b as Element of (R / I) by Th12;
A8: (a * b) - (0. R) = a * b by RLVECT_1:26;
A9: Class (EqRel R,I),(a * b) = x * y by Th14;
assume a * b in I ; :: thesis: ( a in I or b in I )
then Class (EqRel R,I),(a * b) = Class (EqRel R,I),(0. R) by A8, Th6;
then ( x = 0. (R / I) or y = 0. (R / I) ) by A1, A7, A9, VECTSP_2:def 5;
then ( a - (0. R) in I or b - (0. R) in I ) by A1, Th6;
hence ( a in I or b in I ) by RLVECT_1:26; :: thesis: verum