theorem maxirr2: :: RING_2:26

for R being PIDomain
for a being non zero Element of R holds
( {a} -Ideal is maximal iff a is irreducible )