for R being non empty right_complementable right-distributive well-unital add-associative right_zeroed doubleLoopStr
for I being non empty right-ideal Subset of R
for a, b being Element of R st a,b are_congruent_mod I holds
b,a are_congruent_mod I