for R being non empty right_complementable add-associative right_zeroed addLoopStr
for I being non empty add-closed Subset of R
for a, b, c being Element of R st a,b are_congruent_mod I & b,c are_congruent_mod I holds
a,c are_congruent_mod I