let a be Element of R; :: thesis: ( a is irreducible implies a is prime )
assume AS: a is irreducible ; :: thesis: a is prime
then {a} -Ideal is maximal by maxirr2;
hence a is prime by AS, thpr; :: thesis: verum