theorem :: RING_1:15

for R being non empty right_complementable distributive left_unital Abelian add-associative right_zeroed doubleLoopStr
for I being Ideal of R holds Class ((EqRel (R,I)),(1. R)) = 1. (R / I) by Def6;