let R be non degenerated comRing; :: thesis: for a being non zero Element of R holds
( a is prime iff {a} -Ideal is prime )
let a be non zero Element of R; :: thesis: ( a is prime iff {a} -Ideal is prime )
set S = {a} -Ideal ;

A: now :: thesis: ( a is prime implies {a} -Ideal is prime )

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

now :: thesis: for x, y being Element of R holds
( not x * y in {a} -Ideal or x in {a} -Ideal or y in {a} -Ideal )

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

now :: thesis: ( ( a divides x & x in {a} -Ideal ) or ( a divides y & y in {a} -Ideal ) )

per cases ( a divides x or a divides y ) by A2, A0, div0;

case a divides x ; :: thesis: x in {a} -Ideal

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

end;

case a divides y ; :: thesis: y in {a} -Ideal

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

end;

end;

end;

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

end;

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

now :: thesis: {a} -Ideal is proper

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

end;

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

end;

now :: thesis: ( {a} -Ideal is prime implies a is prime )

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

B: now :: thesis: for x, y being Element of R holds
( not a divides x * y or a divides x or a divides y )

let x, y be Element of R; :: thesis: ( not a divides x * y or a divides x or a divides y )
assume a divides x * y ; :: thesis: ( a divides x or a divides y )
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: verum

end;

now :: thesis: not a is unital

assume a is unital ; :: thesis: contradiction
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: verum

end;

hence a is prime by B; :: thesis: verum

end;

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