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

now :: thesis:

assume AS: a is irreducible ; :: thesis:

now :: thesis:

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

now :: thesis:

per cases by AS, H0, H1, div1;

case b is Unit of R ; :: thesis:

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

end;

case b is_associated_to a ; :: thesis:

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

end;

end;

end;

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

end;

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

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

end;

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

end;

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