:: deftheorem defines is_a_irreducible_factor_of FIELD_1:def 1 :
for R being Ring
for a, b being Element of R holds
( b is_a_irreducible_factor_of a iff ( b divides a & b is irreducible ) );