theorem :: RING_1:15

for R being Ring
for I being Ideal of R holds Class ((EqRel (R,I)),(1. R)) = 1. (R / I) by Def6;