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