let R be non degenerated comRing; :: thesis:
let a be non zero Element of R; :: thesis:
set S = {a} -Ideal ;

A: now :: thesis:

assume A0: a is prime ; :: thesis:

now :: thesis:

let x, y be Element of R; :: thesis:
assume A2: x * y in {a} -Ideal ; :: thesis:

now :: thesis:

per cases by A2, A0, div0;

case a divides x ; :: thesis:

hence x in {a} -Ideal by div0; :: thesis:

end;

case a divides y ; :: thesis:

hence y in {a} -Ideal by div0; :: thesis:

end;

end;

end;

hence ( x in {a} -Ideal or y in {a} -Ideal ) ; :: thesis:

end;

then B: {a} -Ideal is quasi-prime by RING_1:def 1;

now :: thesis:

assume not {a} -Ideal is proper ; :: thesis:
then {a} -Ideal = the carrier of R by SUBSET_1:def 6;
then a is unital by div0;
hence contradiction by A0; :: thesis:

end;

hence {a} -Ideal is prime by B; :: thesis:

end;

now :: thesis:

assume A0: {a} -Ideal is prime ; :: thesis:

B: now :: thesis:

let x, y be Element of R; :: thesis:
assume a divides x * y ; :: thesis:
then ( x in {a} -Ideal or y in {a} -Ideal ) by div0, A0, RING_1:def 1;
hence ( a divides x or a divides y ) by div0; :: thesis:

end;

now :: thesis:

assume a is unital ; :: thesis:
then {(1. R)} -Ideal c= {a} -Ideal by div0, IDEAL_1:67;
then the carrier of R c= {a} -Ideal by IDEAL_1:51;
hence contradiction by A0, SUBSET_1:def 6, XBOOLE_0:def 10; :: thesis:

end;

hence a is prime by B; :: thesis:

end;

hence ( a is prime iff {a} -Ideal is prime ) by A; :: thesis: