:: deftheorem defines are_co-prime IDEAL_1:def 22 :
for R being addMagma
for I, J being Subset of R holds
( I,J are_co-prime iff I + J = the carrier of R );