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

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

assume AS: a is irreducible ; :: thesis: {a} -Ideal is maximal

now :: thesis: for J being Ideal of R holds
( not {a} -Ideal c= J or J = {a} -Ideal or not J is proper )

let J be Ideal of R; :: thesis: ( not {a} -Ideal c= J or J = {a} -Ideal or not J is proper )
assume H0: {a} -Ideal c= J ; :: thesis: ( J = {a} -Ideal or not J is proper )
J is principal by IDEAL_1:def 28;
then consider b being Element of R such that
H1: J = {b} -Ideal ;

now :: thesis: ( ( b is Unit of R & not J is proper ) or ( b is_associated_to a & {a} -Ideal = J ) )

per cases ( b is Unit of R or b is_associated_to a ) by AS, H0, H1, div1;

case b is Unit of R ; :: thesis: not J is proper

then J = [#] R by H1, div2;
hence not J is proper ; :: thesis: verum

end;

case b is_associated_to a ; :: thesis: {a} -Ideal = J

hence {a} -Ideal = J by H1, div1; :: thesis: verum

end;

end;

end;

hence ( J = {a} -Ideal or not J is proper ) ; :: thesis: verum

end;

then B: {a} -Ideal is quasi-maximal by RING_1:def 3;

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 AS; :: thesis: verum

end;

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

end;

hence ( {a} -Ideal is maximal iff a is irreducible ) by maxirr; :: thesis: verum