:: deftheorem Def5 defines EqRel RING_1:def 5 :
for R being non empty right_complementable left-distributive left_unital add-associative right_zeroed doubleLoopStr
for I being Ideal of R
for b₃ being Relation of R holds
( b₃ = EqRel (R,I) iff for a, b being Element of R holds
( [a,b] in b₃ iff a - b in I ) );