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

B: now :: thesis:

let x be Element of R; :: thesis:
assume B1: x divides a ; :: thesis:

per cases -Ideal = {x} -Ideal or not {x} -Ideal is proper ) by div1, B1, AS, RING_1:def 3;

case {a} -Ideal = {x} -Ideal ; :: thesis:

hence x is_associated_to a by div1; :: thesis:

end;

case not {x} -Ideal is proper ; :: thesis:

then {x} -Ideal = the carrier of R by SUBSET_1:def 6;
then x is unital by div0;
hence x is Unit of R ; :: thesis:

end;

end;

end;

hence ( x is Unit of R or x is_associated_to a ) ; :: thesis:

end;

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 AS, SUBSET_1:def 6, XBOOLE_0:def 10; :: thesis:

end;

hence a is irreducible by B; :: thesis: