:: deftheorem defines are_congruent_mod POLYRED:def 14 :
for R being non empty addLoopStr
for I being Subset of R
for a, b being Element of R holds
( a,b are_congruent_mod I iff a - b in I );