let R be non degenerated comRing; :: thesis: for a being non zero Element of R st {a} -Ideal is maximal holds
a is irreducible
let a be non zero Element of R; :: thesis: ( {a} -Ideal is maximal implies a is irreducible )
set S = {a} -Ideal ;
assume AS: {a} -Ideal is maximal ; :: thesis: a is irreducible

B: now :: thesis: for x being Element of R holds
( not x divides a or x is Unit of R or x is_associated_to a )

let x be Element of R; :: thesis: ( not x divides a or x is Unit of R or x is_associated_to a )
assume B1: x divides a ; :: thesis: ( x is Unit of R or x is_associated_to a )

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

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

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

hence x is_associated_to a by div1; :: thesis: verum

end;

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

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: verum

end;

end;

end;

hence ( x is Unit of R or x is_associated_to a ) ; :: 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 AS, SUBSET_1:def 6, XBOOLE_0:def 10; :: thesis: verum

end;

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