let x be Element of R; :: thesis: ( x is prime implies x is irreducible )
assume A: x is prime ; :: thesis: x is irreducible

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

let a be Element of R; :: thesis: ( not a divides x or a is Unit of R or a is_associated_to x )
assume C: a divides x ; :: thesis: ( a is Unit of R or a is_associated_to x )
then consider b being Element of R such that
D: a * b = x ;
b <> 0. R by A, D;
then H: b is right_mult-cancelable by ALGSTR_0:def 37;

now :: thesis: ( ( x divides a & a is_associated_to x ) or ( x divides b & a is Unit of R ) )

per cases ( x divides a or x divides b ) by A, D;

case x divides a ; :: thesis: a is_associated_to x

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

end;

case x divides b ; :: thesis: a is Unit of R

then consider c being Element of R such that
F: x * c = b ;
(a * c) * b = x * c by D, GROUP_1:def 3
.= (1. R) * b by F ;
then a divides 1. R by H;
hence a is Unit of R by GCD_1:def 20; :: thesis: verum

end;

end;

end;

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

end;

hence x is irreducible by A; :: thesis: verum