theorem :: RING_1:8

for R being Ring holds Class (EqRel (R,([#] R))) = { the carrier of R}