theorem Th6: :: RING_1:6

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
( Class ((EqRel (R,I)),a) = Class ((EqRel (R,I)),b) iff a - b in I )