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