:: deftheorem Def5 defines EqRel RING_1:def 5 :
for R being Ring
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 ) );