let R be domRing; :: thesis: for a, b being Element of R st a is irreducible & b is_associated_to a holds
b is irreducible
let a, b be Element of R; :: thesis: ( a is irreducible & b is_associated_to a implies b is irreducible )
assume AS: ( a is irreducible & b is_associated_to a ) ; :: thesis: b is irreducible
then consider x being Element of R such that
H: ( x is unital & b * x = a ) by GCD_1:18;
now :: thesis: for c being Element of R holds
( not c divides b or c is Unit of R or c is_associated_to b )
let c be Element of R; :: thesis: ( not c divides b or c is Unit of R or c is_associated_to b )
assume c divides b ; :: thesis: ( c is Unit of R or c is_associated_to b )
then ( c is Unit of R or c is_associated_to a ) by GCD_1:2, AS;
hence ( c is Unit of R or c is_associated_to b ) by AS, GCD_1:4; :: thesis: verum
end;
hence b is irreducible by AS, H; :: thesis: verum