theorem Th5: :: RING_1:5

for R being non empty right_complementable left-distributive left_unital add-associative right_zeroed doubleLoopStr
for I being Ideal of R
for a, b being Element of R holds
( a in Class ((EqRel (R,I)),b) iff a - b in I )