theorem Th7: :: RING_1:7

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